1  /-
  2  Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Zhouhang Zhou
  5  -/
  6  
  7  import measure_theory.simple_func_dense
src         └──────────────────────────────┘
  8  import analysis.normed_space.bounded_linear_maps
src         └───────────────────────────────────────┘
  9  
 10  /-!
 11  # Bochner integral
 12  
 13  The Bochner integral extends the definition of the Lebesgue integral to functions that map from a
 14  measure space into a Banach space (complete normed vector space). It is constructed here by
 15  extending the integral on simple functions.
 16  
 17  ## Main definitions
 18  
 19  The Bochner integral is defined following these steps:
 20  
 21  1. Define the integral on simple functions of the type `simple_func α β` (notation : `α →ₛ β`)
 22    where `β` is a real normed space.
 23  
 24    (See `simple_func.bintegral` and section `bintegral` for details. Also see `simple_func.integral`
 25    for the integral on simple functions of the type `simple_func α ennreal`.)
 26  
 27  2. Use `simple_func α β` to cut out the simple functions from L1 functions, and define integral
 28    on these. The type of simple functions in L1 space is written as `α →₁ₛ β`.
 29  
 30  3. Show that the embedding of `α →₁ₛ β` into L1 is a dense and uniform one.
 31  
 32  4. Show that the integral defined on `α →₁ₛ β` is a continuous linear map.
 33  
 34  5. Define the Bochner integral on L1 functions by extending the integral on integrable simple
 35    functions `α →₁ₛ β` using `continuous_linear_map.extend`. Define the Bochner integral on functions
 36    as the Bochner integral of its equivalence class in L1 space.
 37  
 38  ## Main statements
 39  
 40  1. Basic properties of the Bochner integral on functions of type `α → β`, where `α` is a measure
 41     space and `β` is a real normed space.
 42  
 43    * `integral_zero`                  : `∫ 0 = 0`
 44    * `integral_add`                   : `∫ f + g = ∫ f + ∫ g`
 45    * `integral_neg`                   : `∫ -f = - ∫ f`
 46    * `integral_sub`                   : `∫ f - g = ∫ f - ∫ g`
 47    * `integral_smul`                  : `∫ r • f = r • ∫ f`
 48    * `integral_congr_ae`              : `∀ₘ a, f a = g a → ∫ f = ∫ g`
 49    * `norm_integral_le_integral_norm` : `∥∫ f∥ ≤ ∫ ∥f∥`
 50  
 51  2. Basic properties of the Bochner integral on functions of type `α → ℝ`, where `α` is a measure
 52    space.
 53  
 54    * `integral_nonneg_of_nonneg_ae`  : `∀ₘ a, 0 ≤ f a → 0 ≤ ∫ f`
 55    * `integral_nonpos_of_nonpos_ae`  : `∀ₘ a, f a ≤ 0 → ∫ f ≤ 0`
 56    * `integral_le_integral_of_le_ae` : `∀ₘ a, f a ≤ g a → ∫ f ≤ ∫ g`
 57  
 58  3. Propositions connecting the Bochner integral with the integral on `ennreal`-valued functions,
 59     which is called `lintegral` and has the notation `∫⁻`.
 60  
 61    * `integral_eq_lintegral_max_sub_lintegral_min` : `∫ f = ∫⁻ f⁺ - ∫⁻ f⁻`, where `f⁺` is the positive
 62    part of `f` and `f⁻` is the negative part of `f`.
 63    * `integral_eq_lintegral_of_nonneg_ae`          : `∀ₘ a, 0 ≤ f a → ∫ f = ∫⁻ f`
 64  
 65  4. `tendsto_integral_of_dominated_convergence` : the Lebesgue dominated convergence theorem
 66  
 67  ## Notes
 68  
 69  Some tips on how to prove a proposition if the API for the Bochner integral is not enough so that
 70  you need to unfold the definition of the Bochner integral and go back to simple functions.
 71  
 72  See `integral_eq_lintegral_max_sub_lintegral_min` for a complicated example, which proves that
 73  `∫ f = ∫⁻ f⁺ - ∫⁻ f⁻`, with the first integral sign being the Bochner integral of a real-valued
 74  function f : α → ℝ, and second and third integral sign being the integral on ennreal-valued
 75  functions (called `lintegral`). The proof of `integral_eq_lintegral_max_sub_lintegral_min` is
 76  scattered in sections with the name `pos_part`.
 77  
 78  Here are the usual steps of proving that a property `p`, say `∫ f = ∫⁻ f⁺ - ∫⁻ f⁻`, holds for all
 79  functions :
 80  
 81  1. First go to the `L¹` space.
 82  
 83     For example, if you see `ennreal.to_real (∫⁻ a, ennreal.of_real $ ∥f a∥)`, that is the norm of `f` in
 84  `L¹` space. Rewrite using `l1.norm_of_fun_eq_lintegral_norm`.
 85  
 86  2. Show that the set `{f ∈ L¹ | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻}` is closed in `L¹` using `is_closed_eq`.
 87  
 88  3. Show that the property holds for all simple functions `s` in `L¹` space.
 89  
 90     Typically, you need to convert various notions to their `simple_func` counterpart, using lemmas like
 91  `l1.integral_coe_eq_integral`.
 92  
 93  4. Since simple functions are dense in `L¹`,
 94  ```
 95  univ = closure {s simple}
 96       = closure {s simple | ∫ s = ∫⁻ s⁺ - ∫⁻ s⁻} : the property holds for all simple functions
 97       ⊆ closure {f | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻}
 98       = {f | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻} : closure of a closed set is itself
 99  ```
100  Use `is_closed_property` or `dense_range.induction_on` for this argument.
101  
102  ## Notations
103  
104  * `α →ₛ β`  : simple functions (defined in `measure_theory/integration`)
105  * `α →₁ β`  : functions in L1 space, i.e., equivalence classes of integrable functions (defined in
106               `measure_theory/l1_space`)
107  * `α →₁ₛ β` : simple functions in L1 space, i.e., equivalence classes of integrable simple functions
108  
109  Note : `ₛ` is typed using `\_s`. Sometimes it shows as a box if font is missing.
110  
111  ## Tags
112  
113  Bochner integral, simple function, function space, Lebesgue dominated convergence theorem
114  
115  -/
116  
117  noncomputable theory
118  open_locale classical topological_space
119  
120  set_option class.instance_max_depth 100
doc             └──────────────────────┘
121  
122  -- Typeclass inference has difficulty finding `has_scalar ℝ β` where `β` is a `normed_space` on `ℝ`
123  local attribute [instance, priority 10000]
124    mul_action.to_has_scalar distrib_mul_action.to_mul_action add_comm_group.to_add_comm_monoid
id     └──────────────────────┘ └──────────────────────────────┘ └───────────────────────────────┘
src    └──────────────────────┘ └──────────────────────────────┘ └───────────────────────────────┘
typ    └──────────────────────┘ └──────────────────────────────┘ └───────────────────────────────┘
125    normed_group.to_add_comm_group normed_space.to_module
id     └────────────────────────────┘ └────────────────────┘
src    └────────────────────────────┘ └────────────────────┘
typ    └────────────────────────────┘ └────────────────────┘
126    module.to_semimodule
id     └──────────────────┘
src    └──────────────────┘
typ    └──────────────────┘
127  
128  namespace measure_theory
129  
130  universes u v w
131  variables {α : Type u} [measurable_space α] {β : Type v} [decidable_linear_order β] [has_zero β]
id                           └──────────────┘                  └────────────────────┘     └──────┘
src                          └──────────────┘                  └────────────────────┘     └──────┘
typ                          └──────────────┘                  └────────────────────┘     └──────┘
132  
133  local infixr ` →ₛ `:25 := simple_func
id                             └─────────┘
src                            └─────────┘
typ                            └─────────┘
doc                            └─────────┘
134  
135  namespace simple_func
136  
137  section pos_part
138  
139  /-- Positive part of a simple function. -/
140  def pos_part (f : α →ₛ β) : α →ₛ β := f.map (λb, max b 0)
id                      └┘      └┘     └──┘     └─┘ 
src                      └┘        └┘       └──┘      └─┘
typ                     └┘      └┘     └──┘     └─┘ 
doc                      └┘        └┘       └──┘
141  
142  /-- Negative part of a simple function. -/
143  def neg_part [has_neg β] (f : α →ₛ β) : α →ₛ β := pos_part (-f)
id                 └─────┘         └┘      └┘     └──────┘  
src                └─────┘           └┘        └┘      └──────┘  
typ                └─────┘         └┘      └┘     └──────┘  
doc                                  └┘        └┘      └──────┘
144  
145  lemma pos_part_map_norm (f : α →ₛ ℝ) : (pos_part f).map norm = pos_part f :=
id                                 └┘      └──────┘  └─┘  └──┘  └──────┘ 
src                                 └┘      └──────┘   └─┘  └──┘  └──────┘
typ                                └┘      └──────┘  └─┘  └──┘  └──────┘ 
doc                                 └┘       └──────┘   └─┘         └──────┘
146  begin
st   └─────
147    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
148    rw [map_apply, real.norm_eq_abs, abs_of_nonneg],
id         └───────┘  └──────────────┘  └───────────┘
src    └──┘└───────┘└┘└──────────────┘└┘└───────────┘
typ    └──┘└───────┘└┘└──────────────┘└┘└───────────┘
doc    └──┘         └┘                └┘             
txt    └──┘         └┘                └┘             
par    └──┘         └┘                └┘             
pid      └┘         └┘                └┘             
st   ──────────────┘└────────────────┘└─────────────┘└──
149    rw [pos_part, map_apply],
id         └──────┘  └───────┘
src    └──┘└──────┘└┘└───────┘
typ    └──┘└──────┘└┘└───────┘
doc    └──┘└──────┘└┘         
txt    └──┘        └┘         
par    └──┘        └┘         
pid      └┘        └┘         
st   ─────────────┘└─────────┘└──
150    exact le_max_right _ _
id           └──────────┘
src    └────┘└──────────┘└───┘
typ    └────┘└──────────┘└───┘
doc    └────┘            └───┘
txt    └────┘            └───┘
par    └────┘            └───┘
pid                     └──┘
st   ────────────────────────┘
151  end
st   └─┘
152  
153  lemma neg_part_map_norm (f : α →ₛ ℝ) : (neg_part f).map norm = neg_part f :=
id                                 └┘      └──────┘  └─┘  └──┘  └──────┘ 
src                                 └┘      └──────┘   └─┘  └──┘  └──────┘
typ                                └┘      └──────┘  └─┘  └──┘  └──────┘ 
doc                                 └┘       └──────┘   └─┘         └──────┘
154  by { rw neg_part, exact pos_part_map_norm _ }
id           └──────┘        └───────────────┘
src       └─┘└──────┘  └────┘└───────────────┘└─┘
typ       └─┘└──────┘  └────┘└───────────────┘└─┘
doc       └─┘└──────┘  └────┘                 └─┘
txt       └─┘          └────┘                 └─┘
par       └─┘          └────┘                 └─┘
pid                                         └┘
st     └────────────┘└──────────────────────────┘└┘
155  
156  lemma pos_part_sub_neg_part (f : α →ₛ ℝ) : f.pos_part - f.neg_part = f :=
id                                     └┘     └───────┘  └───────┘  
src                                     └┘      └───────┘   └───────┘ 
typ                                    └┘     └───────┘  └───────┘  
doc                                     └┘       └───────┘    └───────┘
157  begin
st   └─────
158    simp only [pos_part, neg_part],
id                └──────┘  └──────┘
src    └─────────┘└──────┘└┘└──────┘
typ    └─────────┘└──────┘└┘└──────┘
doc    └─────────┘└──────┘└┘└──────┘
txt    └─────────┘        └┘        
par    └─────────┘        └┘        
pid        └──┘└┘        └┘        
st   ───────────────────────────────┘└─
159    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
160    exact max_zero_sub_eq_self (f a)
id           └──────────────────┘   
src    └────┘└──────────────────┘   └┘
typ    └────┘└──────────────────┘ └┘
doc    └────┘                       └┘
txt    └────┘                       └┘
par    └────┘                       └┘
pid                                
st   ──────────────────────────────────┘
161  end
st   └─┘
162  
163  end pos_part
164  
165  end simple_func
166  
167  end measure_theory
168  
169  namespace measure_theory
170  open set lattice filter topological_space ennreal emetric
171  
172  universes u v w
173  variables {α : Type u} [measure_space α] {β : Type v} {γ : Type w}
id                          └───────────┘
src                          └───────────┘
typ                         └───────────┘
doc                          └───────────┘
174  
175  local infixr ` →ₛ `:25 := simple_func
id                             └─────────┘
src                            └─────────┘
typ                            └─────────┘
doc                            └─────────┘
176  
177  namespace simple_func
178  
179  section bintegral
180  /-!
181  ### The Bochner integral of simple functions
182  
183  Define the Bochner integral of simple functions of the type `α →ₛ β` where `β` is a normed group,
184  and prove basic property of this integral.
185  -/
186  open finset
187  
188  variables [normed_group β] [normed_group γ]
id              └──────────┘     └──────────┘
src             └──────────┘     └──────────┘
typ             └──────────┘     └──────────┘
doc             └──────────┘     └──────────┘
189  
190  lemma integrable_iff_integral_lt_top {f : α →ₛ β} :
id                                              └┘ 
src                                              └┘
typ                                             └┘ 
doc                                              └┘
191    integrable f ↔ integral (f.map (coe ∘ nnnorm)) < ⊤ :=
id     └────────┘   └──────┘  └──┘  └─┘  └────┘    
src    └────────┘    └──────┘   └──┘  └─┘  └────┘    
typ    └────────┘   └──────┘  └──┘  └─┘  └────┘    
doc    └────────┘     └──────┘   └──┘        └────┘
192  by { rw [integrable, ← lintegral_eq_integral, lintegral_map] }
id            └────────┘    └───────────────────┘  └───────────┘
src       └──┘└────────┘└──┘└───────────────────┘└┘└───────────┘└┘
typ       └──┘└────────┘└──┘└───────────────────┘└┘└───────────┘└┘
doc       └──┘└────────┘└──┘                     └┘             └┘
txt       └──┘          └──┘                     └┘             └┘
par       └──┘          └──┘                     └┘             └┘
pid         └┘          └──┘                     └┘             
st     └───────────────┘└───────────────────────┘└─────────────┘└┘
193  
194  lemma fin_vol_supp_of_integrable {f : α →ₛ β} (hf : integrable f) : f.fin_vol_supp :=
id                                          └┘         └────────┘     └───────────┘
src                                          └┘          └────────┘       └───────────┘
typ                                         └┘         └────────┘     └───────────┘
doc                                          └┘          └────────┘
195  begin
st   └─────
196    rw [integrable_iff_integral_lt_top] at hf,
id         └────────────────────────────┘
src    └──┘└────────────────────────────┘└─────┘
typ    └──┘└────────────────────────────┘└─────┘
doc    └──┘                              └─────┘
txt    └──┘                              └─────┘
par    └──┘                              └─────┘
pid      └┘                              └────┘
st   ───────────────────────────────────┘└────┘└─
197    have hf := fin_vol_supp_of_integral_lt_top hf,
id                └─────────────────────────────┘ └┘
src    └─────────┘└─────────────────────────────┘
typ    └─────────┘└─────────────────────────────┘└┘
doc    └─────────┘                               
txt    └─────────┘                               
par    └─────────┘                               
pid    └─────┘└─┘                               
st   ──────────────────────────────────────────────┘└─
198    refine fin_vol_supp_of_fin_vol_supp_map f hf _,
id            └──────────────────────────────┘  └┘
src    └─────┘└──────────────────────────────┘   └┘
typ    └─────┘└──────────────────────────────┘└┘└┘
doc    └─────┘                                   └┘
txt    └─────┘                                   └┘
par    └─────┘                                   └┘
pid                                             └┘
st   ───────────────────────────────────────────────┘└─
199    assume b, simp [nnnorm_eq_zero]
id                     └────────────┘
src    └──────┘  └────┘└────────────┘└┘
typ    └──────┘  └────┘└────────────┘└┘
doc    └──────┘  └────┘              └┘
txt    └──────┘  └────┘              └┘
par    └──────┘  └────┘              └┘
pid    └──────┘                    
st   ─────────┘└──────────────────────┘
200  end
st   └─┘
201  
202  lemma integrable_of_fin_vol_supp {f : α →ₛ β} (h : f.fin_vol_supp) : integrable f :=
id                                          └┘        └───────────┘    └────────┘ 
src                                          └┘          └───────────┘    └────────┘
typ                                         └┘        └───────────┘    └────────┘ 
doc                                          └┘                           └────────┘
203  by { rw [integrable_iff_integral_lt_top], exact integral_map_coe_lt_top h nnnorm_zero }
id            └────────────────────────────┘         └─────────────────────┘  └─────────┘
src       └──┘└────────────────────────────┘  └────┘└─────────────────────┘ └─────────┘
typ       └──┘└────────────────────────────┘  └────┘└─────────────────────┘└─────────┘
doc       └──┘                                └────┘└─────────────────────┘            
txt       └──┘                                └────┘                                   
par       └──┘                                └────┘                                   
pid         └┘                                                                        
st     └───────────────────────────────────┘└─────────────────────────────────────────────┘└┘
204  
205  /-- For simple functions with a `normed_group` as codomain, being integrable is the same as having
206      finite volume support. -/
207  lemma integrable_iff_fin_vol_supp (f : α →ₛ β) : integrable f ↔ f.fin_vol_supp :=
id                                           └┘     └────────┘   └───────────┘
src                                           └┘      └────────┘     └───────────┘
typ                                          └┘     └────────┘   └───────────┘
doc                                           └┘      └────────┘
208  iff.intro fin_vol_supp_of_integrable integrable_of_fin_vol_supp
id   └───────┘ └────────────────────────┘ └────────────────────────┘
src  └───────┘ └────────────────────────┘ └────────────────────────┘
typ  └───────┘ └────────────────────────┘ └────────────────────────┘
209  
210  lemma integrable_pair {f : α →ₛ β} {g : α →ₛ γ} (hf : integrable f) (hg : integrable g) :
id                               └┘         └┘         └────────┘         └────────┘ 
src                               └┘           └┘          └────────┘          └────────┘
typ                              └┘         └┘         └────────┘         └────────┘ 
doc                               └┘           └┘          └────────┘          └────────┘
211    integrable (pair f g) :=
id     └────────┘  └──┘  
src    └────────┘  └──┘
typ    └────────┘  └──┘  
doc    └────────┘  └──┘
212  by { rw integrable_iff_fin_vol_supp at *, apply fin_vol_supp_pair; assumption }
id           └─────────────────────────┘             └───────────────┘
src       └─┘└─────────────────────────┘└───┘  └────┘└───────────────┘  └─────────┘
typ       └─┘└─────────────────────────┘└───┘  └────┘└───────────────┘  └─────────┘
doc       └─┘└─────────────────────────┘└───┘  └────┘                   └─────────┘
txt       └─┘                           └───┘  └────┘                   └─────────┘
par       └─┘                           └───┘  └────┘                   └─────────┘
pid                                    └───┘                                    
st     └────────────────────────────────────┘└────────────────────────────────────┘└┘
213  
214  variables [normed_space ℝ γ]
id              └──────────┘ 
src             └──────────┘ 
typ             └──────────┘ 
doc             └──────────┘
215  
216  /-- Bochner integral of simple functions whose codomain is a real `normed_space`.
217      The name `simple_func.integral` has been taken in the file `integration.lean`, which calculates
218      the integral of a simple function with type `α → ennreal`.
219      The name `bintegral` stands for Bochner integral. -/
220  def bintegral [normed_space ℝ β] (f : α →ₛ β) : β :=
id                  └──────────┘          └┘     
src                 └──────────┘            └┘
typ                 └──────────┘          └┘     
doc                 └──────────┘             └┘
221  f.range.sum (λ x, (ennreal.to_real (volume (f ⁻¹' {x}))) • x)
id   └────┘└──┘       └─────────────┘  └────┘   └─┘       
src   └────┘└──┘        └─────────────┘  └────┘    └─┘       
typ  └────┘└──┘       └─────────────┘  └────┘   └─┘       
doc   └────┘            └─────────────┘            └─┘
222  
223  /-- Calculate the integral of `g ∘ f : α →ₛ γ`, where `f` is an integrable function from `α` to `β`
224      and `g` is a function from `β` to `γ`. We require `g 0 = 0` so that `g ∘ f` is integrable. -/
225  lemma map_bintegral (f : α →ₛ β) (g : β → γ) (hf : integrable f) (hg : g 0 = 0) :
id                             └┘                   └────────┘            
src                             └┘                      └────────┘              
typ                            └┘                   └────────┘            
doc                             └┘                      └────────┘
226    (f.map g).bintegral = f.range.sum (λ x, (ennreal.to_real (volume (f ⁻¹' {x}))) • (g x)) :=
id      └──┘  └───────┘   └────┘└──┘       └─────────────┘  └────┘   └─┘         
src      └──┘   └───────┘    └────┘└──┘        └─────────────┘  └────┘    └─┘       
typ     └──┘  └───────┘   └────┘└──┘       └─────────────┘  └────┘   └─┘         
doc      └──┘   └───────┘     └────┘            └─────────────┘            └─┘
227  begin
st   └─────
228    /- Just a complicated calculation with `finset.sum`. Real work is done by
st   ────────────────────────────────────────────────────────────────────────────
229       `map_preimage_singleton`, `simple_func.volume_bUnion_preimage` and `ennreal.to_real_sum`  -/
st   ──────────────────────────────────────────────────────────────────────────────────────────────────
230    rw integrable_iff_fin_vol_supp at hf,
id        └─────────────────────────┘
src    └─┘└─────────────────────────┘└────┘
typ    └─┘└─────────────────────────┘└────┘
doc    └─┘└─────────────────────────┘└────┘
txt    └─┘                           └────┘
par    └─┘                           └────┘
pid                                 └────┘
st   ─────────────────────────────────────┘└─
231    simp only [bintegral, range_map],
id                └───────┘  └───────┘
src    └─────────┘└───────┘└┘└───────┘
typ    └─────────┘└───────┘└┘└───────┘
doc    └─────────┘└───────┘└┘         
txt    └─────────┘         └┘         
par    └─────────┘         └┘         
pid        └──┘└┘         └┘         
st   ─────────────────────────────────┘└─
232    refine finset.sum_image' _ (assume b hb, _),
id            └───────────────┘
src    └─────┘└───────────────┘└─┘       └───────┘
typ    └─────┘└───────────────┘└─┘       └───────┘
doc    └─────┘                 └─┘       └───────┘
txt    └─────┘                 └─┘       └───────┘
par    └─────┘                 └─┘       └───────┘
pid                           └─┘       └───────┘
st   ────────────────────────────────────────────┘└─
233    rcases mem_range.1 hb with ⟨a, rfl⟩,
id            └───────┘   └┘
src    └─────┘└───────┘└─┘  └────────────┘
typ    └─────┘└───────┘└─┘└┘└────────────┘
doc    └─────┘         └─┘  └────────────┘
txt    └─────┘         └─┘  └────────────┘
par    └─────┘         └─┘  └────────────┘
pid                   └─┘  └────────────┘
st   ────────────────────────────────────┘└─
234    let s' := f.range.filter (λb, g b = g (f a)),
id               └────────────┘              
src    └────────┘└────────────┘  └─┘      └┘
typ    └────────┘└────────────┘  └─┘   └┘
doc    └────────┘└────────────┘  └─┘       └┘
txt    └────────┘                └─┘       └┘
par    └────────┘                └─┘       └┘
pid    └────┘└─┘                └─┘       └┘
st   ─────────────────────────────────────────────┘└─
235    calc (ennreal.to_real (volume ((f.map g) ⁻¹' {g (f a)}))) • (g (f a)) =
id     └──┘                            └───┘    └─┘             
src    └──┘                            └───┘    └─┘             
typ    └──┘                            └───┘    └─┘             
doc    └──┘                            └───┘    └─┘
st   ──────────────────────────────────────────────────────────────────────────
236        (ennreal.to_real (volume (⋃b∈s', f ⁻¹' {b}))) • (g (f a)) : by rw map_preimage_singleton
id          └─────────────┘  └────┘   └┘                               └────────────────────┘
src         └─────────────┘  └────┘                                     └─┘└────────────────────┘
typ         └─────────────┘  └────┘   └┘                            └─┘└────────────────────┘
doc         └─────────────┘                                             └─┘                      
txt                                                                       └─┘                      
par                                                                       └─┘                      
pid                                                                                               
st   ───────────────────────────────────────────────────────────────────┘└──────────────────────────
237    ... = (ennreal.to_real (s'.sum (λb, volume (f ⁻¹' {b})))) • (g (f a)) :
id                             └────┘   
src  ─┘                        └────┘
typ  ─┘                        └────┘   
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└───────────────────────────────────────────────────────────────────────
238      by rw volume_bUnion_preimage
id             └────────────────────┘
src         └─┘└────────────────────┘
typ         └─┘└────────────────────┘
doc         └─┘                      
txt         └─┘                      
par         └─┘                      
pid                                 
st   ─────┘└──────────────────────────
239    ... = (s'.sum (λb, ennreal.to_real (volume (f ⁻¹' {b})))) • (g (f a)) :
id                     
src  ─┘
typ  ─┘                
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└───────────────────────────────────────────────────────────────────────
240    begin
st   ─┘└─────
241      by_cases h : g (f a) = 0,
id                       
src      └───────┘ └─┘    └┘ └┘
typ      └───────┘ └─┘ └┘ └┘
doc      └───────┘ └─┘    └┘ └┘
txt      └───────┘ └─┘    └┘ └┘
par      └───────┘ └─┘    └┘ └┘
pid               └─┘    └┘ 
st   ───────────────────────────┘└─
242      { rw [h, smul_zero, smul_zero] },
id               └───────┘  └───────┘
src        └──┘ └┘└───────┘└┘└───────┘└┘
typ        └──┘└┘└───────┘└┘└───────┘└┘
doc        └──┘ └┘         └┘         └┘
txt        └──┘ └┘         └┘         └┘
par        └──┘ └┘         └┘         └┘
pid          └┘ └┘         └┘         
st   ─────┘└───┘└─────────┘└─────────┘└┘
243      { rw ennreal.to_real_sum,
id            └─────────────────┘
src        └─┘└─────────────────┘
typ        └─┘└─────────────────┘
doc        └─┘└─────────────────┘
txt        └─┘
par        └─┘
pid          
st   ───────────────────────────┘└─
244        simp only [mem_filter],
id                    └────────┘
src        └─────────┘└────────┘
typ        └─────────┘└────────┘
doc        └─────────┘          
txt        └─────────┘          
par        └─────────┘          
pid            └──┘└┘          
st   ───────────────────────────┘└─
245        rintros b ⟨_, hb⟩,
src        └───────────────┘
typ        └───────────────┘
doc        └───────────────┘
txt        └───────────────┘
par        └───────────────┘
pid               └────────┘
st   ──────────────────────┘└─
246        have : b ≠ 0, { assume hb', rw [← hb, hb'] at h, contradiction },
id                                         └┘  └─┘
src        └─────┘ └┘    └────────┘  └────┘  └┘   └────┘  └────────────┘
typ        └─────┘└┘    └────────┘  └────┘└┘└┘└─┘└────┘  └────────────┘
doc        └─────┘  └┘    └────────┘  └────┘  └┘   └────┘  └────────────┘
txt        └─────┘  └┘    └────────┘  └────┘  └┘   └────┘  └────────────┘
par        └─────┘  └┘    └────────┘  └────┘  └┘   └────┘  └────────────┘
pid        └───┘└┘      └────────┘    └──┘  └┘   └───┘               
st   ─────────────────┘└──┘└────────┘└────────┘└───┘└───┘└──────────────┘└┘
247        apply hf,
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────────────┘└─
248        assumption }
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid                  
st   ────────────────┘└─
249    end
st   ────┘
250    ... = s'.sum (λb, (ennreal.to_real (volume (f ⁻¹' {b}))) • (g (f a))) : finset.sum_smul
id                                                                            └─────────────┘
src                                                                            └─────────────┘
typ                                                                           └─────────────┘
st   ──────────────────────────────────────────────────────────────────────────────────────────
251    ... = s'.sum (λb, (ennreal.to_real (volume (f ⁻¹' {b}))) • (g b)) :
id                    
typ                   
st   ──────────────────────────────────────────────────────────────────────
252      finset.sum_congr rfl $ by { assume x, simp only [mem_filter], rintro ⟨_, h⟩, rw h }
id       └──────────────┘ └─┘                             └────────┘                     
src      └──────────────┘ └─┘        └──────┘  └─────────┘└────────┘  └───────────┘  └─┘ 
typ      └──────────────┘ └─┘        └──────┘  └─────────┘└────────┘  └───────────┘  └─┘
doc                                  └──────┘  └─────────┘            └───────────┘  └─┘ 
txt                                  └──────┘  └─────────┘            └───────────┘  └─┘ 
par                                  └──────┘  └─────────┘            └───────────┘  └─┘ 
pid                                  └──────┘      └──┘└┘                  └─────┘     
st   ────────────────────────────┘└─────────┘└──────────────────────┘└─────────────┘└─────┘└─
253  end
st   ──┘
254  
255  /-- `simple_func.bintegral` and `simple_func.integral` agree when the integrand has type
256      `α →ₛ ennreal`. But since `ennreal` is not a `normed_space`, we need some form of coercion.
257      See `bintegral_eq_integral'` for a simpler version. -/
258  lemma bintegral_eq_integral {f : α →ₛ β} {g : β → ennreal} (hf : integrable f) (hg0 : g 0 = 0)
id                                     └┘           └─────┘        └────────┘             
src                                     └┘             └─────┘        └────────┘               
typ                                    └┘           └─────┘        └────────┘             
doc                                     └┘             └─────┘        └────────┘
259    (hgt : ∀b, g b < ⊤):
id                  
src                    
typ                 
260    (f.map (ennreal.to_real ∘ g)).bintegral = ennreal.to_real (f.map g).integral :=
id      └──┘  └─────────────┘    └───────┘   └─────────────┘  └──┘  └──────┘
src      └──┘  └─────────────┘     └───────┘   └─────────────┘   └──┘   └──────┘
typ     └──┘  └─────────────┘    └───────┘   └─────────────┘  └──┘  └──────┘
doc      └──┘  └─────────────┘      └───────┘    └─────────────┘   └──┘   └──────┘
261  begin
st   └─────
262    have hf' : f.fin_vol_supp, { rwa integrable_iff_fin_vol_supp at hf },
id                └────────────┘        └─────────────────────────┘
src    └─────────┘└────────────┘    └──┘└─────────────────────────┘└─────┘
typ    └─────────┘└────────────┘    └──┘└─────────────────────────┘└─────┘
doc    └─────────┘                  └──┘└─────────────────────────┘└─────┘
txt    └─────────┘                  └──┘                           └─────┘
par    └─────────┘                  └──┘                           └─────┘
pid    └──────┘└─┘                                                └────┘
st   ──────────────────────────┘└──┘└────────────────────────────────────┘└┘
263    rw [map_bintegral f _ hf, map_integral, ennreal.to_real_sum],
id         └───────────┘    └┘  └──────────┘  └─────────────────┘
src    └──┘└───────────┘ └─┘  └┘└──────────┘└┘└─────────────────┘
typ    └──┘└───────────┘└─┘└┘└┘└──────────┘└┘└─────────────────┘
doc    └──┘└───────────┘ └─┘  └┘└──────────┘└┘└─────────────────┘
txt    └──┘              └─┘  └┘            └┘                   
par    └──┘              └─┘  └┘            └┘                   
pid      └┘              └─┘  └┘            └┘                   
st   ─────────────────────────┘└────────────┘└───────────────────┘└──
264    { refine finset.sum_congr rfl (λb hb, _),
id              └──────────────┘ └─┘
src      └─────┘└──────────────┘└─┘  └──────┘
typ      └─────┘└──────────────┘└─┘  └──────┘
doc      └─────┘                     └──────┘
txt      └─────┘                     └──────┘
par      └─────┘                     └──────┘
pid                                 └──────┘
st   ───┘└────────────────────────────────────┘└─
265      rw [smul_eq_mul],
id           └─────────┘
src      └──┘└─────────┘
typ      └──┘└─────────┘
doc      └──┘           
txt      └──┘           
par      └──┘           
pid        └┘           
st   ──────────────────┘└──
266      rw [to_real_mul_to_real, mul_comm] },
id           └─────────────────┘  └──────┘
src      └──┘└─────────────────┘└┘└──────┘└┘
typ      └──┘└─────────────────┘└┘└──────┘└┘
doc      └──┘                   └┘        └┘
txt      └──┘                   └┘        └┘
par      └──┘                   └┘        └┘
pid        └┘                   └┘        
st   ──────────────────────────┘└────────┘└┘
267    { assume a ha,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
268      by_cases a0 : a = 0,
id                      
src      └───────┘  └─┘ └┘
typ      └───────┘  └─┘└┘
doc      └───────┘  └─┘  └┘
txt      └───────┘  └─┘  └┘
par      └───────┘  └─┘  └┘
pid                └─┘  
st   ──────────────────────┘└─
269      { rw [a0, hg0, zero_mul], exact with_top.zero_lt_top },
id             └┘  └─┘  └──────┘         └──────────────────┘
src        └──┘  └┘   └┘└──────┘  └────┘└──────────────────┘
typ        └──┘└┘└┘└─┘└┘└──────┘  └────┘└──────────────────┘
doc        └──┘  └┘   └┘          └────┘                    
txt        └──┘  └┘   └┘          └────┘                    
par        └──┘  └┘   └┘          └────┘                    
pid          └┘  └┘   └┘                                   
st   ─────┘└────┘└───┘└────────┘└────────────────────────────┘└┘
270      apply mul_lt_top (hgt a) (hf' _ a0) },
id             └────────┘  └─┘    └─┘   └┘
src      └────┘└────────┘     └┘    └─┘  └┘
typ      └────┘└────────┘ └─┘└┘ └─┘└─┘└┘└┘
doc      └────┘               └┘    └─┘  └┘
txt      └────┘               └┘    └─┘  └┘
par      └────┘               └┘    └─┘  └┘
pid                          └┘    └─┘  
st   ───────────────────────────────────────┘└┘
271    { simp [hg0] }
id             └─┘
src      └────┘   └┘
typ      └────┘└─┘└┘
doc      └────┘   └┘
txt      └────┘   └┘
par      └────┘   └┘
pid             
st   ──────────────┘└─
272  end
st   ──┘
273  
274  /-- `simple_func.bintegral` and `lintegral : (α → ennreal) → ennreal` are the same when the
275      integrand has type `α →ₛ ennreal`. But since `ennreal` is not a `normed_space`, we need some
276      form of coercion.
277      See `bintegral_eq_lintegral'` for a simpler version. -/
278  lemma bintegral_eq_lintegral (f : α →ₛ β) (g : β → ennreal) (hf : integrable f) (hg0 : g 0 = 0)
id                                      └┘           └─────┘        └────────┘             
src                                      └┘             └─────┘        └────────┘               
typ                                     └┘           └─────┘        └────────┘             
doc                                      └┘             └─────┘        └────────┘
279    (hgt : ∀b, g b < ⊤):
id                  
src                    
typ                 
280    (f.map (ennreal.to_real ∘ g)).bintegral = ennreal.to_real (∫⁻ a, g (f a)) :=
id      └──┘  └─────────────┘    └───────┘   └─────────────┘  └┘     
src      └──┘  └─────────────┘     └───────┘   └─────────────┘  └┘  
typ     └──┘  └─────────────┘    └───────┘   └─────────────┘  └┘     
doc      └──┘  └─────────────┘      └───────┘    └─────────────┘  └┘  
281  by { rw [bintegral_eq_integral hf hg0 hgt, ← lintegral_eq_integral], refl }
id            └───────────────────┘ └┘ └─┘ └─┘    └───────────────────┘
src       └──┘└───────────────────┘        └──┘└───────────────────┘  └───┘
typ       └──┘└───────────────────┘└┘└─┘└─┘└──┘└───────────────────┘  └───┘
doc       └──┘└───────────────────┘        └──┘                       └───┘
txt       └──┘                             └──┘                       └───┘
par       └──┘                             └──┘                       └───┘
pid         └┘                             └──┘                           
st     └─────────────────────────────────────┘└───────────────────────┘└──────┘└┘
282  
283  variables [normed_space ℝ β]
id              └──────────┘ 
src             └──────────┘ 
typ             └──────────┘ 
doc             └──────────┘
284  
285  lemma bintegral_congr {f g : α →ₛ β} (hf : integrable f) (hg : integrable g) (h : ∀ₘ a, f a = g a):
id                                 └┘         └────────┘         └────────┘        └┘      
src                                 └┘          └────────┘          └────────┘         └┘       
typ                                └┘         └────────┘         └────────┘        └┘      
doc                                 └┘          └────────┘          └────────┘         └┘  
286    bintegral f = bintegral g :=
id     └───────┘   └───────┘ 
src    └───────┘    └───────┘
typ    └───────┘   └───────┘ 
doc    └───────┘     └───────┘
287  show ((pair f g).map prod.fst).bintegral = ((pair f g).map prod.snd).bintegral, from
id          └──┘   └─┘  └──────┘ └───────┘     └──┘   └─┘  └──────┘ └───────┘
src         └──┘     └─┘  └──────┘ └───────┘     └──┘     └─┘  └──────┘ └───────┘
typ         └──┘   └─┘  └──────┘ └───────┘     └──┘   └─┘  └──────┘ └───────┘
doc         └──┘     └─┘           └───────┘      └──┘     └─┘           └───────┘
288  begin
st   └─────
289    have inte := integrable_pair hf hg,
id                  └─────────────┘ └┘ └┘
src    └───────────┘└─────────────┘  
typ    └───────────┘└─────────────┘└┘└┘
doc    └───────────┘                 
txt    └───────────┘                 
par    └───────────┘                 
pid    └───────┘└─┘                 
st   ───────────────────────────────────┘└─
290    rw [map_bintegral (pair f g) _ inte prod.fst_zero, map_bintegral (pair f g) _ inte prod.snd_zero],
id         └───────────┘  └──┘      └──┘ └───────────┘  └───────────┘  └──┘      └──┘ └───────────┘
src    └──┘└───────────┘ └──┘  └──┘    └───────────┘└┘└───────────┘ └──┘  └──┘    └───────────┘
typ    └──┘└───────────┘ └──┘└──┘└──┘└───────────┘└┘└───────────┘ └──┘└──┘└──┘└───────────┘
doc    └──┘└───────────┘ └──┘  └──┘                 └┘└───────────┘ └──┘  └──┘                 
txt    └──┘                    └──┘                 └┘                    └──┘                 
par    └──┘                    └──┘                 └┘                    └──┘                 
pid      └┘                    └──┘                 └┘                    └──┘                 
st   ──────────────────────────────────────────────────┘└─────────────────────────────────────────────┘└──
291    refine finset.sum_congr rfl (assume p hp, _),
id            └──────────────┘ └─┘
src    └─────┘└──────────────┘└─┘       └───────┘
typ    └─────┘└──────────────┘└─┘       └───────┘
doc    └─────┘                          └───────┘
txt    └─────┘                          └───────┘
par    └─────┘                          └───────┘
pid                                    └───────┘
st   ─────────────────────────────────────────────┘└─
292    rcases mem_range.1 hp with ⟨a, rfl⟩,
id            └───────┘   └┘
src    └─────┘└───────┘└─┘  └────────────┘
typ    └─────┘└───────┘└─┘└┘└────────────┘
doc    └─────┘         └─┘  └────────────┘
txt    └─────┘         └─┘  └────────────┘
par    └─────┘         └─┘  └────────────┘
pid                   └─┘  └────────────┘
st   ────────────────────────────────────┘└─
293    by_cases eq : f a = g a,
id                        
src    └───────┘  └─┘   
typ    └───────┘  └─┘ 
doc    └───────┘  └─┘    
txt    └───────┘  └─┘    
par    └───────┘  └─┘    
pid              └─┘    
st   ────────────────────────┘└─
294    { dsimp only [pair_apply], rw eq },
id                   └────────┘      └┘
src      └──────────┘└────────┘  └─┘└┘
typ      └──────────┘└────────┘  └─┘└┘
doc      └──────────┘            └─┘  
txt      └──────────┘            └─┘  
par      └──────────┘            └─┘  
pid           └───┘└┘                
st   ───┘└─────────────────────┘└──────┘└┘
295    { have : volume ((pair f g) ⁻¹' {(f a, g a)}) = 0,
id              └────┘   └──┘      └─┘      
src      └─────┘└────┘  └──┘  └┘└─┘  └┘  └──┘ └┘
typ      └─────┘└────┘  └──┘  └┘└─┘ └┘└──┘ └┘
doc      └─────┘        └──┘  └┘└─┘    └┘  └──┘ └┘
txt      └─────┘              └┘       └┘  └──┘ └┘
par      └─────┘              └┘       └┘  └──┘ └┘
pid      └───┘└┘              └┘       └┘  └──┘ 
st   ──────────────────────────────────────────────────┘└─
296      { refine volume_mono_null (assume a' ha', _) h,
id                └──────────────┘                    
src        └─────┘└──────────────┘       └──────────┘
typ        └─────┘└──────────────┘       └──────────┘
doc        └─────┘                       └──────────┘
txt        └─────┘                       └──────────┘
par        └─────┘                       └──────────┘
pid                                     └──────────┘
st   ─────┘└──────────────────────────────────────────┘└─
297        simp only [set.mem_preimage, mem_singleton_iff, pair_apply, prod.mk.inj_iff] at ha',
id                    └──────────────┘  └───────────────┘  └────────┘  └─────────────┘
src        └─────────┘└──────────────┘└┘└───────────────┘└┘└────────┘└┘└─────────────┘└──────┘
typ        └─────────┘└──────────────┘└┘└───────────────┘└┘└────────┘└┘└─────────────┘└──────┘
doc        └─────────┘                └┘                 └┘          └┘               └──────┘
txt        └─────────┘                └┘                 └┘          └┘               └──────┘
par        └─────────┘                └┘                 └┘          └┘               └──────┘
pid            └──┘└┘                └┘                 └┘          └┘               └────┘
st   ────────────────────────────────────────────────────────────────────────────────────────┘└─
298        show f a' ≠ g a',
id                    └┘
src        └───┘    
typ        └───┘  └┘
doc        └───┘     
txt        └───┘     
par        └───┘     
pid        └───┘     
st   ─────────────────────┘└─
299        rwa [ha'.1, ha'.2] },
id              └─┘    └─┘
src        └───┘   └──┘   └──┘
typ        └───┘└─┘└──┘└─┘└──┘
doc        └───┘   └──┘   └──┘
txt        └───┘   └──┘   └──┘
par        └───┘   └──┘   └──┘
pid           └┘   └──┘   └─┘
st   ─────────────┘└─────┘└─┘└┘
300      simp only [this, pair_apply, zero_smul, ennreal.zero_to_real] },
id                  └──┘  └────────┘  └───────┘  └──────────────────┘
src      └─────────┘    └┘└────────┘└┘└───────┘└┘└──────────────────┘└┘
typ      └─────────┘└──┘└┘└────────┘└┘└───────┘└┘└──────────────────┘└┘
doc      └─────────┘    └┘          └┘         └┘                    └┘
txt      └─────────┘    └┘          └┘         └┘                    └┘
par      └─────────┘    └┘          └┘         └┘                    └┘
pid          └──┘└┘    └┘          └┘         └┘                    
st   ─────────────────────────────────────────────────────────────────┘└──
301  end
st   ──┘
302  
303  /-- `simple_func.bintegral` and `simple_func.integral` agree when the integrand has type
304      `α →ₛ ennreal`. But since `ennreal` is not a `normed_space`, we need some form of coercion. -/
305  lemma bintegral_eq_integral' {f : α →ₛ ℝ} (hf : integrable f) (h_pos : ∀ₘ a, 0 ≤ f a) :
id                                      └┘         └────────┘            └┘      
src                                      └┘         └────────┘             └┘     
typ                                     └┘         └────────┘            └┘      
doc                                      └┘          └────────┘             └┘  
306    f.bintegral = ennreal.to_real (f.map ennreal.of_real).integral :=
id     └────────┘  └─────────────┘  └──┘ └─────────────┘ └──────┘
src     └────────┘  └─────────────┘   └──┘ └─────────────┘ └──────┘
typ    └────────┘  └─────────────┘  └──┘ └─────────────┘ └──────┘
doc     └────────┘   └─────────────┘   └──┘ └─────────────┘ └──────┘
307  begin
st   └─────
308    have : ∀ₘ a, f a = (f.map (ennreal.to_real ∘ ennreal.of_real)) a,
id            └┘         └───┘  └─────────────┘  └─────────────┘
src    └─────┘└┘└┘   └───┘ └─────────────┘└─────────────┘└─┘
typ    └─────┘└┘└┘   └───┘ └─────────────┘└─────────────┘└─┘
doc    └─────┘└┘└┘    └───┘ └─────────────┘ └─────────────┘└─┘
txt    └─────┘  └┘                                          └─┘
par    └─────┘  └┘                                          └─┘
pid    └───┘└┘  └┘                                          └─┘
st   ─────────────────────────────────────────────────────────────────┘└─
309    { filter_upwards [h_pos],
src      └──────────────┘     
typ      └──────────────┘     
doc      └──────────────┘     
txt      └──────────────┘     
par      └──────────────┘     
pid                    └┘     
st   ───┘└────────────────────┘└─
310      assume a,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
311      simp only [mem_set_of_eq, map_apply, function.comp_apply],
id                  └───────────┘  └───────┘  └─────────────────┘
src      └─────────┘└───────────┘└┘└───────┘└┘└─────────────────┘
typ      └─────────┘└───────────┘└┘└───────┘└┘└─────────────────┘
doc      └─────────┘             └┘         └┘                   
txt      └─────────┘             └┘         └┘                   
par      └─────────┘             └┘         └┘                   
pid          └──┘└┘             └┘         └┘                   
st   ────────────────────────────────────────────────────────────┘└─
312      assume h,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
313      exact (ennreal.to_real_of_real h).symm },
id              └─────────────────────┘ 
src      └────┘ └─────────────────────┘ └─────┘
typ      └────┘ └─────────────────────┘└─────┘
doc      └────┘                         └─────┘
txt      └────┘                         └─────┘
par      └────┘                         └─────┘
pid                                    └───┘└┘
st   ──────────────────────────────────────────┘└┘
314    rw ← bintegral_eq_integral hf,
id          └───────────────────┘ └┘
src    └───┘└───────────────────┘
typ    └───┘└───────────────────┘└┘
doc    └───┘└───────────────────┘
txt    └───┘                     
par    └───┘                     
pid      └─┘                     
st   ──────────────────────────────┘└─
315    { refine bintegral_congr hf _ this, exact integrable_of_ae_eq hf this },
id              └─────────────┘ └┘   └──┘        └─────────────────┘ └┘ └──┘
src      └─────┘└─────────────┘  └─┘      └────┘└─────────────────┘      
typ      └─────┘└─────────────┘└┘└─┘└──┘  └────┘└─────────────────┘└┘└──┘
doc      └─────┘                 └─┘      └────┘                         
txt      └─────┘                 └─┘      └────┘                         
par      └─────┘                 └─┘      └────┘                         
pid                             └─┘                                    
st   ───┘└──────────────────────────────┘└──────────────────────────────────┘└┘
316    { exact ennreal.of_real_zero },
id             └──────────────────┘
src      └────┘└──────────────────┘
typ      └────┘└──────────────────┘
doc      └────┘                    
txt      └────┘                    
par      └────┘                    
pid                               
st   ───┘└─────────────────────────┘└┘
317    { assume b, rw ennreal.lt_top_iff_ne_top, exact ennreal.of_real_ne_top  }
id                    └───────────────────────┘        └────────────────────┘
src      └──────┘  └─┘└───────────────────────┘  └────┘└────────────────────┘└┘
typ      └──────┘  └─┘└───────────────────────┘  └────┘└────────────────────┘└┘
doc      └──────┘  └─┘                           └────┘                      └┘
txt      └──────┘  └─┘                           └────┘                      └┘
par      └──────┘  └─┘                           └────┘                      └┘
pid      └──────┘                                                          └┘
st   ───────────┘└────────────────────────────┘└──────────────────────────────┘└─
318  end
st   ──┘
319  
320  /-- `simple_func.bintegral` and `lintegral : (α → ennreal) → ennreal` agree when the integrand has
321      type `α →ₛ ennreal`. But since `ennreal` is not a `normed_space`, we need some form of coercion. -/
322  lemma bintegral_eq_lintegral' {f : α →ₛ ℝ} (hf : integrable f) (h_pos : ∀ₘ a, 0 ≤ f a) :
id                                       └┘         └────────┘            └┘      
src                                       └┘         └────────┘             └┘     
typ                                      └┘         └────────┘            └┘      
doc                                       └┘          └────────┘             └┘  
323    f.bintegral = ennreal.to_real (∫⁻ a, (f.map ennreal.of_real a)) :=
id     └────────┘  └─────────────┘  └┘   └──┘ └─────────────┘ 
src     └────────┘  └─────────────┘  └┘     └──┘ └─────────────┘
typ    └────────┘  └─────────────┘  └┘   └──┘ └─────────────┘ 
doc     └────────┘   └─────────────┘  └┘     └──┘ └─────────────┘
324  by rw [bintegral_eq_integral' hf h_pos, ← lintegral_eq_integral]
id          └────────────────────┘ └┘ └───┘    └───────────────────┘
src     └──┘└────────────────────┘       └──┘└───────────────────┘└─
typ     └──┘└────────────────────┘└┘└───┘└──┘└───────────────────┘└─
doc     └──┘└────────────────────┘       └──┘                     └─
txt     └──┘                             └──┘                     └─
par     └──┘                             └──┘                     └─
pid       └┘                             └──┘                     
st     └──────────────────────────────────┘└───────────────────────┘
325  
src  
typ  
doc  
txt  
par  
pid  
st   
326  lemma bintegral_add {f g : α →ₛ β} (hf : integrable f) (hg : integrable g) :
id                               └┘         └────────┘         └────────┘ 
src                               └┘          └────────┘          └────────┘
typ                              └┘         └────────┘         └────────┘ 
doc                               └┘          └────────┘          └────────┘
327    bintegral (f + g) = bintegral f + bintegral g :=
id     └───────┘       └───────┘   └───────┘ 
src    └───────┘         └───────┘    └───────┘
typ    └───────┘       └───────┘   └───────┘ 
doc    └───────┘           └───────┘     └───────┘
328  calc bintegral (f + g) = sum (pair f g).range
id        └───────┘        └─┘  └──┘   └───┘
src       └───────┘          └─┘  └──┘     └───┘
typ       └───────┘        └─┘  └──┘   └───┘
doc       └───────┘                └──┘     └───┘
329         (λx, ennreal.to_real (volume ((pair f g) ⁻¹' {x})) • (x.fst + x.snd)) :
id              └─────────────┘  └────┘   └──┘    └─┘       └──┘  └──┘
src              └─────────────┘  └────┘   └──┘      └─┘         └──┘   └──┘
typ             └─────────────┘  └────┘   └──┘    └─┘       └──┘  └──┘
doc              └─────────────┘           └──┘      └─┘
330  begin
st   └─────
331    rw [add_eq_map₂, map_bintegral (pair f g)],
id         └─────────┘  └───────────┘  └──┘  
src    └──┘└─────────┘└┘└───────────┘ └──┘  └┘
typ    └──┘└─────────┘└┘└───────────┘ └──┘└┘
doc    └──┘           └┘└───────────┘ └──┘  └┘
txt    └──┘           └┘                    └┘
par    └──┘           └┘                    └┘
pid      └┘           └┘                    └┘
st   ────────────────┘└────────────────────────┘└──
332    { exact integrable_pair hf hg },
id             └─────────────┘ └┘ └┘
src      └────┘└─────────────┘    
typ      └────┘└─────────────┘└┘└┘
doc      └────┘                   
txt      └────┘                   
par      └────┘                   
pid                              
st   ───┘└──────────────────────────┘└┘
333    { simp only [add_zero, prod.fst_zero, prod.snd_zero] }
id                  └──────┘  └───────────┘  └───────────┘
src      └─────────┘└──────┘└┘└───────────┘└┘└───────────┘└┘
typ      └─────────┘└──────┘└┘└───────────┘└┘└───────────┘└┘
doc      └─────────┘        └┘             └┘             └┘
txt      └─────────┘        └┘             └┘             └┘
par      └─────────┘        └┘             └┘             └┘
pid          └──┘└┘        └┘             └┘             
st   ──────────────────────────────────────────────────────┘└─
334  end
st   ──┘
335  ... = sum (pair f g).range
id         └─┘  └──┘   └───┘
src        └─┘  └──┘     └───┘
typ        └─┘  └──┘   └───┘
doc             └──┘     └───┘
336          (λx, ennreal.to_real (volume ((pair f g) ⁻¹' {x})) • x.fst +
id               └─────────────┘  └────┘   └──┘    └─┘      └──┘ 
src               └─────────────┘  └────┘   └──┘      └─┘        └──┘ 
typ              └─────────────┘  └────┘   └──┘    └─┘      └──┘ 
doc               └─────────────┘           └──┘      └─┘
337               ennreal.to_real (volume ((pair f g) ⁻¹' {x})) • x.snd) :
id                └─────────────┘  └────┘   └──┘    └─┘      └──┘
src               └─────────────┘  └────┘   └──┘      └─┘        └──┘
typ               └─────────────┘  └────┘   └──┘    └─┘      └──┘
doc               └─────────────┘           └──┘      └─┘
338    finset.sum_congr rfl $ assume a ha, smul_add _ _ _
id     └──────────────┘ └─┘           └┘  └──────┘
src    └──────────────┘ └─┘                └──────┘
typ    └──────────────┘ └─┘           └┘  └──────┘
339  ... = sum (simple_func.range (pair f g))
id         └─┘  └───────────────┘  └──┘  
src        └─┘  └───────────────┘  └──┘
typ        └─┘  └───────────────┘  └──┘  
doc             └───────────────┘  └──┘
340          (λ (x : β × β), ennreal.to_real (volume ((pair f g) ⁻¹' {x})) • x.fst) +
id                        └─────────────┘  └────┘   └──┘    └─┘      └──┘  
src                         └─────────────┘  └────┘   └──┘      └─┘        └──┘  
typ                       └─────────────┘  └────┘   └──┘    └─┘      └──┘  
doc                          └─────────────┘           └──┘      └─┘
341        sum (simple_func.range (pair f g))
id         └─┘  └───────────────┘  └──┘  
src        └─┘  └───────────────┘  └──┘
typ        └─┘  └───────────────┘  └──┘  
doc             └───────────────┘  └──┘
342          (λ (x : β × β), ennreal.to_real (volume ((pair f g) ⁻¹' {x})) • x.snd) :
id                        └─────────────┘  └────┘   └──┘    └─┘      └──┘
src                         └─────────────┘  └────┘   └──┘      └─┘        └──┘
typ                       └─────────────┘  └────┘   └──┘    └─┘      └──┘
doc                          └─────────────┘           └──┘      └─┘
343    by rw finset.sum_add_distrib
id           └────────────────────┘
src       └─┘└────────────────────┘
typ       └─┘└────────────────────┘
doc       └─┘                      
txt       └─┘                      
par       └─┘                      
pid                               
st       └─────────────────────────┘
344  ... = ((pair f g).map prod.fst).bintegral + ((pair f g).map prod.snd).bintegral :
id           └──┘   └─┘  └──────┘ └───────┘     └──┘   └─┘  └──────┘ └───────┘
src          └──┘     └─┘  └──────┘ └───────┘     └──┘     └─┘  └──────┘ └───────┘
typ          └──┘   └─┘  └──────┘ └───────┘     └──┘   └─┘  └──────┘ └───────┘
doc          └──┘     └─┘           └───────┘      └──┘     └─┘           └───────┘
345  begin
st   └─────
346    rw [map_bintegral (pair f g), map_bintegral (pair f g)],
id         └───────────┘  └──┘     └───────────┘  └──┘  
src    └──┘└───────────┘ └──┘  └─┘└───────────┘ └──┘  └┘
typ    └──┘└───────────┘ └──┘└─┘└───────────┘ └──┘└┘
doc    └──┘└───────────┘ └──┘  └─┘└───────────┘ └──┘  └┘
txt    └──┘                    └─┘                    └┘
par    └──┘                    └─┘                    └┘
pid      └┘                    └─┘                    └┘
st   ─────────────────────────────┘└────────────────────────┘└──
347    { exact integrable_pair hf hg }, { refl },
id             └─────────────┘ └┘ └┘
src      └────┘└─────────────┘         └───┘
typ      └────┘└─────────────┘└┘└┘     └───┘
doc      └────┘                        └───┘
txt      └────┘                        └───┘
par      └────┘                        └───┘
pid                                       
st   ───┘└──────────────────────────┘└┘└─┘└───┘└┘
348    { exact integrable_pair hf hg }, { refl }
id             └─────────────┘ └┘ └┘
src      └────┘└─────────────┘         └───┘
typ      └────┘└─────────────┘└┘└┘     └───┘
doc      └────┘                        └───┘
txt      └────┘                        └───┘
par      └────┘                        └───┘
pid                                       
st   ───┘└──────────────────────────┘└┘└──────┘└─
349  end
st   ──┘
350  ... = bintegral f + bintegral g : rfl
id         └───────┘   └───────┘    └─┘
src        └───────┘    └───────┘     └─┘
typ        └───────┘   └───────┘    └─┘
doc        └───────┘     └───────┘
351  
352  lemma bintegral_neg {f : α →ₛ β} (hf : integrable f) : bintegral (-f) = - bintegral f :=
id                             └┘         └────────┘     └───────┘      └───────┘ 
src                             └┘          └────────┘      └───────┘       └───────┘
typ                            └┘         └────────┘     └───────┘      └───────┘ 
doc                             └┘          └────────┘      └───────┘          └───────┘
353  calc bintegral (-f) = bintegral (f.map (has_neg.neg)) : rfl
id        └───────┘      └───────┘  └──┘  └─────────┘     └─┘
src       └───────┘       └───────┘   └──┘  └─────────┘     └─┘
typ       └───────┘      └───────┘  └──┘  └─────────┘     └─┘
doc       └───────┘        └───────┘   └──┘
354    ... = - bintegral f :
id            └───────┘ 
src           └───────┘
typ           └───────┘ 
doc            └───────┘
355    begin
st     └─────
356      rw [map_bintegral f _ hf neg_zero, bintegral, ← sum_neg_distrib],
id           └───────────┘    └┘ └──────┘  └───────┘    └─────────────┘
src      └──┘└───────────┘ └─┘  └──────┘└┘└───────┘└──┘└─────────────┘
typ      └──┘└───────────┘└─┘└┘└──────┘└┘└───────┘└──┘└─────────────┘
doc      └──┘└───────────┘ └─┘          └┘└───────┘└──┘               
txt      └──┘              └─┘          └┘         └──┘               
par      └──┘              └─┘          └┘         └──┘               
pid        └┘              └─┘          └┘         └──┘               
st   ────────────────────────────────────┘└─────────┘└─────────────────┘└──
357      refine finset.sum_congr rfl (λx h, smul_neg _ _),
id              └──────────────┘ └─┘        └──────┘
src      └─────┘└──────────────┘└─┘  └───┘└──────┘└───┘
typ      └─────┘└──────────────┘└─┘  └───┘└──────┘└───┘
doc      └─────┘                     └───┘        └───┘
txt      └─────┘                     └───┘        └───┘
par      └─────┘                     └───┘        └───┘
pid                                 └───┘        └───┘
st   ───────────────────────────────────────────────────┘└─
358    end
st   ────┘
359  
360  lemma bintegral_sub {f g : α →ₛ β} (hf : integrable f) (hg : integrable g) :
id                               └┘         └────────┘         └────────┘ 
src                               └┘          └────────┘          └────────┘
typ                              └┘         └────────┘         └────────┘ 
doc                               └┘          └────────┘          └────────┘
361    bintegral (f - g) = bintegral f - bintegral g :=
id     └───────┘       └───────┘   └───────┘ 
src    └───────┘         └───────┘    └───────┘
typ    └───────┘       └───────┘   └───────┘ 
doc    └───────┘           └───────┘     └───────┘
362  begin
st   └─────
363    have : f - g = f + (-g) := rfl,
id                          └─┘
src    └─────┘     └───┘└─┘
typ    └─────┘   └───┘└─┘
doc    └─────┘         └───┘
txt    └─────┘         └───┘
par    └─────┘         └───┘
pid    └───┘└┘         └──┘
st   ───────────────────────────────┘└─
364    rw [this, bintegral_add hf _, bintegral_neg hg],
id         └──┘  └───────────┘ └┘    └───────────┘ └┘
src    └──┘    └┘└───────────┘  └──┘└───────────┘  
typ    └──┘└──┘└┘└───────────┘└┘└──┘└───────────┘└┘
doc    └──┘    └┘               └──┘               
txt    └──┘    └┘               └──┘               
par    └──┘    └┘               └──┘               
pid      └┘    └┘               └──┘               
st   ─────────┘└──────────────────┘└────────────────┘└──
365    { refl },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ───┘└───┘└┘
366    exact hg.neg
id           └────┘
src    └────┘└────┘
typ    └────┘└────┘
doc    └────┘      
txt    └────┘      
par    └────┘      
pid               
st   ──────────────┘
367  end
st   └─┘
368  
369  lemma bintegral_smul (r : ℝ) {f : α →ₛ β} (hf : integrable f) :
id                                     └┘         └────────┘ 
src                                     └┘          └────────┘
typ                                    └┘         └────────┘ 
doc                                      └┘          └────────┘
370    bintegral (r • f) = r • bintegral f :=
id     └───────┘         └───────┘ 
src    └───────┘            └───────┘
typ    └───────┘         └───────┘ 
doc    └───────┘               └───────┘
371  calc bintegral (r • f) = sum f.range (λx, ennreal.to_real (volume (f ⁻¹' {x})) • r • x) :
id        └───────┘        └─┘ └────┘     └─────────────┘  └────┘   └─┘        
src       └───────┘          └─┘  └────┘      └─────────────┘  └────┘    └─┘         
typ       └───────┘        └─┘ └────┘     └─────────────┘  └────┘   └─┘        
doc       └───────┘                └────┘      └─────────────┘            └─┘
372    by rw [smul_eq_map r f, map_bintegral f _ hf (smul_zero _)]
id            └─────────┘    └───────────┘    └┘  └───────┘
src       └──┘└─────────┘  └┘└───────────┘ └─┘   └───────┘└───┘
typ       └──┘└─────────┘└┘└───────────┘└─┘└┘ └───────┘└───┘
doc       └──┘             └┘└───────────┘ └─┘            └───┘
txt       └──┘             └┘              └─┘            └───┘
par       └──┘             └┘              └─┘            └───┘
pid         └┘             └┘              └─┘            └──┘
st       └──────────────────┘└──────────────────────────────────┘
373  ... = (f.range).sum (λ (x : β), ((ennreal.to_real (volume (f ⁻¹' {x}))) * r) • x) :
id          └────┘ └─┘               └─────────────┘  └────┘   └─┘          
src          └────┘ └─┘                └─────────────┘  └────┘    └─┘           
typ         └────┘ └─┘               └─────────────┘  └────┘   └─┘          
doc          └────┘                    └─────────────┘            └─┘
374    finset.sum_congr rfl $ λb hb, by apply smul_smul
id     └──────────────┘ └─┘     └┘           └───────┘
src    └──────────────┘ └─┘             └────┘└───────┘
typ    └──────────────┘ └─┘     └┘     └────┘└───────┘
doc                                     └────┘         
txt                                     └────┘         
par                                     └────┘         
pid                                                   
st                                     └───────────────┘
375  ... = r • bintegral f :
id           └───────┘ 
src           └───────┘
typ          └───────┘ 
doc            └───────┘
376  begin
st   └─────
377    rw [bintegral, smul_sum],
id         └───────┘  └──────┘
src    └──┘└───────┘└┘└──────┘
typ    └──┘└───────┘└┘└──────┘
doc    └──┘└───────┘└┘        
txt    └──┘         └┘        
par    └──┘         └┘        
pid      └┘         └┘        
st   ──────────────┘└────────┘└──
378    refine finset.sum_congr rfl (λb hb, _),
id            └──────────────┘ └─┘
src    └─────┘└──────────────┘└─┘  └──────┘
typ    └─────┘└──────────────┘└─┘  └──────┘
doc    └─────┘                     └──────┘
txt    └─────┘                     └──────┘
par    └─────┘                     └──────┘
pid                               └──────┘
st   ───────────────────────────────────────┘└─
379    rw [smul_smul, mul_comm]
id         └───────┘  └──────┘
src    └──┘└───────┘└┘└──────┘└┘
typ    └──┘└───────┘└┘└──────┘└┘
doc    └──┘         └┘        └┘
txt    └──┘         └┘        └┘
par    └──┘         └┘        └┘
pid      └┘         └┘        
st   ──────────────┘└────────┘
380  end
st   └─┘
381  
382  lemma norm_bintegral_le_bintegral_norm (f : α →ₛ β) (hf : integrable f) :
id                                                └┘         └────────┘ 
src                                                └┘          └────────┘
typ                                               └┘         └────────┘ 
doc                                                └┘          └────────┘
383    ∥f.bintegral∥ ≤ (f.map norm).bintegral :=
id     └────────┘   └──┘ └──┘ └───────┘
src     └────────┘    └──┘ └──┘ └───────┘
typ    └────────┘   └──┘ └──┘ └───────┘
doc      └────────┘      └──┘      └───────┘
384  begin
st   └─────
385    rw map_bintegral f norm hf norm_zero,
id        └───────────┘  └──┘ └┘ └───────┘
src    └─┘└───────────┘ └──┘  └───────┘
typ    └─┘└───────────┘└──┘└┘└───────┘
doc    └─┘└───────────┘       
txt    └─┘                    
par    └─┘                    
pid                          
st   ─────────────────────────────────────┘└─
386    rw bintegral,
id        └───────┘
src    └─┘└───────┘
typ    └─┘└───────┘
doc    └─┘└───────┘
txt    └─┘
par    └─┘
pid      
st   ─────────────┘└─
387    calc ∥sum f.range (λx, ennreal.to_real (volume (f ⁻¹' {x})) • x)∥ ≤
id     └──┘                                             └─┘      
src    └──┘                                              └─┘      
typ    └──┘                                             └─┘      
doc    └──┘                                              └─┘
st   ──────────────────────────────────────────────────────────────────────
388         sum f.range (λx, ∥ennreal.to_real (volume (f ⁻¹' {x})) • x∥) :
id                        
typ                       
st   ──────────────────────────────────────────────────────────────────────
389      norm_sum_le _ _
id       └─────────┘
src      └─────────┘
typ      └─────────┘
st   ────────────────────
390      ... = sum f.range (λx, ennreal.to_real (volume (f ⁻¹' {x})) • ∥x∥) :
id             └─┘ └─────┘     └─────────────┘  └────┘  
src            └─┘ └─────┘      └─────────────┘  └────┘
typ            └─┘ └─────┘     └─────────────┘  └────┘  
doc                └─────┘      └─────────────┘
st   ─────────────────────────────────────────────────────────────────────────
391      begin
st   ───┘└─────
392        refine finset.sum_congr rfl (λb hb, _),
id                └──────────────┘ └─┘
src        └─────┘└──────────────┘└─┘  └──────┘
typ        └─────┘└──────────────┘└─┘  └──────┘
doc        └─────┘                     └──────┘
txt        └─────┘                     └──────┘
par        └─────┘                     └──────┘
pid                                   └──────┘
st   ───────────────────────────────────────────┘└─
393        rw [norm_smul, smul_eq_mul, real.norm_eq_abs, abs_of_nonneg to_real_nonneg]
id             └───────┘  └─────────┘  └──────────────┘  └───────────┘ └────────────┘
src        └──┘└───────┘└┘└─────────┘└┘└──────────────┘└┘└───────────┘└────────────┘└─
typ        └──┘└───────┘└┘└─────────┘└┘└──────────────┘└┘└───────────┘└────────────┘└─
doc        └──┘         └┘           └┘                └┘                           └─
txt        └──┘         └┘           └┘                └┘                           └─
par        └──┘         └┘           └┘                └┘                           └─
pid          └┘         └┘           └┘                └┘                           
st   ──────────────────┘└───────────┘└────────────────┘└────────────────────────────┘
394      end
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└───
395  end
st   ──┘
396  
397  end bintegral
398  
399  end simple_func
400  
401  namespace l1
402  
403  open ae_eq_fun
404  
405  variables [normed_group β] [second_countable_topology β]
id              └──────────┘     └───────────────────────┘
src             └──────────┘     └───────────────────────┘
typ             └──────────┘     └───────────────────────┘
doc             └──────────┘     └───────────────────────┘
406            [normed_group γ] [second_countable_topology γ]
id              └──────────┘     └───────────────────────┘
src             └──────────┘     └───────────────────────┘
typ             └──────────┘     └───────────────────────┘
doc             └──────────┘     └───────────────────────┘
407  
408  variables (α β)
409  /-- `l1.simple_func` is a subspace of L1 consisting of equivalence classes of an integrable simple
410      function. -/
411  def simple_func : Type (max u v) :=
412  { f : α →₁ β // ∃ (s : α →ₛ β),  integrable s ∧ ae_eq_fun.mk s s.measurable = f}
id         └┘            └┘    └────────┘   └──────────┘  └─────────┘  
src         └┘              └┘     └────────┘    └──────────┘    └─────────┘ 
typ        └┘            └┘    └────────┘   └──────────┘  └─────────┘  
doc          └┘               └┘      └────────┘     └──────────┘    └─────────┘
413  
414  variables {α β}
415  
416  infixr ` →₁ₛ `:25 := measure_theory.l1.simple_func
id                        └───────────────────────────┘
src                       └───────────────────────────┘
typ                       └───────────────────────────┘
doc                       └───────────────────────────┘
417  
418  namespace simple_func
419  
420  section instances
421  /-! Simple functions in L1 space form a `normed_space`. -/
422  
423  instance : has_coe (α →₁ₛ β) (α →₁ β) := ⟨subtype.val⟩
id              └─────┘   └─┘     └┘       └─────────┘
src             └─────┘    └─┘       └┘        └─────────┘
typ             └─────┘   └─┘     └┘       └─────────┘
doc                        └─┘       └┘
424  
425  protected lemma eq {f g : α →₁ₛ β} : (f : α →₁ β) = (g : α →₁ β) → f = g := subtype.eq
id                              └─┘          └┘         └┘           └────────┘
src                              └─┘             └┘            └┘              └────────┘
typ                             └─┘          └┘         └┘           └────────┘
doc                              └─┘             └┘             └┘
426  protected lemma eq' {f g : α →₁ₛ β} : (f : α →ₘ β) = (g : α →ₘ β) → f = g := subtype.eq ∘ subtype.eq
id                               └─┘          └┘         └┘           └────────┘  └────────┘
src                               └─┘             └┘            └┘              └────────┘  └────────┘
typ                              └─┘          └┘         └┘           └────────┘  └────────┘
doc                               └─┘             └┘             └┘
427  
428  @[elim_cast] protected lemma eq_iff {f g : α →₁ₛ β} : (f : α →₁ β) = (g : α →₁ β) ↔ f = g :=
id                                               └─┘          └┘         └┘      
src                                               └─┘             └┘            └┘       
typ                                              └─┘          └┘         └┘      
doc    └───────┘                                  └─┘             └┘             └┘
429  iff.intro (subtype.eq) (congr_arg coe)
id   └───────┘  └────────┘   └───────┘ └─┘
src  └───────┘  └────────┘   └───────┘ └─┘
typ  └───────┘  └────────┘   └───────┘ └─┘
430  
431  @[elim_cast] protected lemma eq_iff' {f g : α →₁ₛ β} : (f : α →ₘ β) = (g : α →ₘ β) ↔ f = g :=
id                                                └─┘          └┘         └┘      
src                                                └─┘             └┘            └┘       
typ                                               └─┘          └┘         └┘      
doc    └───────┘                                   └─┘             └┘             └┘
432  iff.intro (simple_func.eq') (congr_arg _)
id   └───────┘  └─────────────┘   └───────┘
src  └───────┘  └─────────────┘   └───────┘
typ  └───────┘  └─────────────┘   └───────┘
433  
434  /-- L1 simple functions forms a `emetric_space`, with the emetric being inherited from L1 space,
435    i.e., `edist f g = ∫⁻ a, edist (f a) (g a)`.
436    Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
437    integral. -/
438  protected def emetric_space  : emetric_space (α →₁ₛ β) := subtype.emetric_space
id                                  └───────────┘   └─┘      └───────────────────┘
src                                 └───────────┘    └─┘       └───────────────────┘
typ                                 └───────────┘   └─┘      └───────────────────┘
doc                                 └───────────┘    └─┘       └───────────────────┘
439  
440  /-- L1 simple functions forms a `metric_space`, with the metric being inherited from L1 space,
441    i.e., `dist f g = ennreal.to_real (∫⁻ a, edist (f a) (g a)`).
442    Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
443    integral. -/
444  protected def metric_space : metric_space (α →₁ₛ β) := subtype.metric_space
id                                └──────────┘   └─┘      └──────────────────┘
src                               └──────────┘    └─┘       └──────────────────┘
typ                               └──────────┘   └─┘      └──────────────────┘
doc                               └──────────┘    └─┘
445  
446  local attribute [instance] protected lemma is_add_subgroup : is_add_subgroup
id                                                                └─────────────┘
src                                                               └─────────────┘
typ                                                               └─────────────┘
doc                                                               └─────────────┘
447    (λf:α →₁ β, ∃ (s : α →ₛ β), integrable s ∧ ae_eq_fun.mk s s.measurable = f) :=
id          └┘          └┘   └────────┘   └──────────┘  └─────────┘  
src          └┘            └┘    └────────┘    └──────────┘    └─────────┘ 
typ         └┘          └┘   └────────┘   └──────────┘  └─────────┘  
doc          └┘             └┘     └────────┘     └──────────┘    └─────────┘
448  { zero_mem := by { use 0, split, { apply integrable_zero }, { refl } },
id                                            └─────────────┘
src                     └───┘  └───┘    └────┘└─────────────┘     └───┘
typ                     └───┘  └───┘    └────┘└─────────────┘     └───┘
doc                     └───┘  └───┘    └────┘                    └───┘
txt                     └───┘  └───┘    └────┘                    └───┘
par                     └───┘  └───┘    └────┘                    └───┘
pid                                                                
st                   └──────┘└─────┘└──┘└────────────────────┘└┘└──────┘└──┘
449    add_mem :=
450    begin
st     └─────
451      rintros f g ⟨s, hsi, hs⟩ ⟨t, hti, ht⟩,
src      └───────────────────────────────────┘
typ      └───────────────────────────────────┘
doc      └───────────────────────────────────┘
txt      └───────────────────────────────────┘
par      └───────────────────────────────────┘
pid             └────────────────────────────┘
st   ────────────────────────────────────────┘└─
452      use s + t, split,
id             
src      └──┘    └───┘
typ      └──┘  └───┘
doc      └──┘     └───┘
txt      └──┘     └───┘
par      └──┘     └───┘
pid           
st   ────────────┘└─────┘└─
453      { exact hsi.add s.measurable t.measurable hti },
id               └─────┘ └──────────┘ └──────────┘ └─┘
src        └────┘└─────┘└──────────┘└──────────┘   
typ        └────┘└─────┘└──────────┘└──────────┘└─┘
doc        └────┘       └──────────┘└──────────┘   
txt        └────┘                                  
par        └────┘                                  
pid                                               
st   ─────┘└──────────────────────────────────────────┘└┘
454      { rw [coe_add, ← hs, ← ht], refl }
id             └─────┘    └┘    └┘
src        └──┘└─────┘└──┘  └──┘    └───┘
typ        └──┘└─────┘└──┘└┘└──┘└┘  └───┘
doc        └──┘       └──┘  └──┘    └───┘
txt        └──┘       └──┘  └──┘    └───┘
par        └──┘       └──┘  └──┘    └───┘
pid          └┘       └──┘  └──┘        
st   ────────────────┘└────┘└────┘└──────┘└─
455    end,
st   ────┘
456    neg_mem :=
457    begin
st     └─────
458      rintros f ⟨s, hsi, hs⟩,
src      └────────────────────┘
typ      └────────────────────┘
doc      └────────────────────┘
txt      └────────────────────┘
par      └────────────────────┘
pid             └─────────────┘
st   ─────────────────────────┘└─
459      use -s, split,
id           
src      └──┘   └───┘
typ      └──┘  └───┘
doc      └──┘    └───┘
txt      └──┘    └───┘
par      └──┘    └───┘
pid         
st   ─────────┘└─────┘└─
460      { exact hsi.neg },
id               └─────┘
src        └────┘└─────┘
typ        └────┘└─────┘
doc        └────┘       
txt        └────┘       
par        └────┘       
pid                    
st   ─────┘└────────────┘└┘
461      { rw [coe_neg, ← hs], refl }
id             └─────┘    └┘
src        └──┘└─────┘└──┘    └───┘
typ        └──┘└─────┘└──┘└┘  └───┘
doc        └──┘       └──┘    └───┘
txt        └──┘       └──┘    └───┘
par        └──┘       └──┘    └───┘
pid          └┘       └──┘        
st   ────────────────┘└────┘└──────┘└─
462    end }
st   ────┘
463  
464  /-- Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
465    integral. -/
466  protected def add_comm_group : add_comm_group (α →₁ₛ β) := subtype.add_comm_group
id                                  └────────────┘   └─┘      └────────────────────┘
src                                 └────────────┘    └─┘       └────────────────────┘
typ                                 └────────────┘   └─┘      └────────────────────┘
doc                                                   └─┘
467  
468  local attribute [instance] simple_func.add_comm_group simple_func.metric_space
id                              └────────────────────────┘ └──────────────────────┘
src                             └────────────────────────┘ └──────────────────────┘
typ                             └────────────────────────┘ └──────────────────────┘
doc                             └────────────────────────┘ └──────────────────────┘
469    simple_func.emetric_space
id     └───────────────────────┘
src    └───────────────────────┘
typ    └───────────────────────┘
doc    └───────────────────────┘
470  
471  instance : inhabited (α →₁ₛ β) := ⟨0⟩
id              └───────┘   └─┘ 
src             └───────┘    └─┘
typ             └───────┘   └─┘ 
doc                          └─┘
472  
473  @[simp, elim_cast] lemma coe_zero : ((0 : α →₁ₛ β) : α →₁ β) = 0 := rfl
id                                              └─┘      └┘         └─┘
src                                              └─┘        └┘          └─┘
typ                                             └─┘      └┘         └─┘
doc    └──┘  └───────┘                           └─┘        └┘
474  @[simp, move_cast] lemma coe_add (f g : α →₁ₛ β) : ((f + g : α →₁ₛ β) : α →₁ β) = f + g := rfl
id                                            └─┘             └─┘      └┘          └─┘
src                                            └─┘                 └─┘        └┘             └─┘
typ                                           └─┘             └─┘      └┘          └─┘
doc    └──┘  └───────┘                         └─┘                  └─┘        └┘
475  @[simp, move_cast] lemma coe_neg (f : α →₁ₛ β) : ((-f : α →₁ₛ β) : α →₁ β) = -f := rfl
id                                          └─┘           └─┘      └┘        └─┘
src                                          └─┘              └─┘        └┘          └─┘
typ                                         └─┘           └─┘      └┘        └─┘
doc    └──┘  └───────┘                       └─┘               └─┘        └┘
476  @[simp, move_cast] lemma coe_sub (f g : α →₁ₛ β) : ((f - g : α →₁ₛ β) : α →₁ β) = f - g := rfl
id                                            └─┘             └─┘      └┘          └─┘
src                                            └─┘                 └─┘        └┘             └─┘
typ                                           └─┘             └─┘      └┘          └─┘
doc    └──┘  └───────┘                         └─┘                  └─┘        └┘
477  @[simp] lemma edist_eq (f g : α →₁ₛ β) : edist f g = edist (f : α →₁ β) (g : α →₁ β) := rfl
id                                  └─┘     └───┘    └───┘      └┘        └┘      └─┘
src                                  └─┘      └───┘      └───┘        └┘           └┘       └─┘
typ                                 └─┘     └───┘    └───┘      └┘        └┘      └─┘
doc    └──┘                          └─┘                               └┘           └┘
478  @[simp] lemma dist_eq (f g : α →₁ₛ β) : dist f g = dist (f : α →₁ β) (g : α →₁ β) := rfl
id                                 └─┘     └──┘    └──┘      └┘        └┘      └─┘
src                                 └─┘      └──┘      └──┘        └┘           └┘       └─┘
typ                                └─┘     └──┘    └──┘      └┘        └┘      └─┘
doc    └──┘                         └─┘                             └┘           └┘
479  
480  /-- The norm on `α →₁ₛ β` is inherited from L1 space. That is, `∥f∥ = ∫⁻ a, edist (f a) 0`.
481    Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
482    integral. -/
483  protected def has_norm : has_norm (α →₁ₛ β) := ⟨λf, ∥(f : α →₁ β)∥⟩
id                            └──────┘   └─┘               └┘  
src                           └──────┘    └─┘                   └┘   
typ                           └──────┘   └─┘               └┘  
doc                           └──────┘    └─┘                    └┘
484  
485  local attribute [instance] simple_func.has_norm
id                              └──────────────────┘
src                             └──────────────────┘
typ                             └──────────────────┘
doc                             └──────────────────┘
486  
487  lemma norm_eq (f : α →₁ₛ β) : ∥f∥ = ∥(f : α →₁ β)∥ := rfl
id                       └─┘            └┘      └─┘
src                       └─┘                └┘       └─┘
typ                      └─┘            └┘      └─┘
doc                       └─┘                    └┘
488  lemma norm_eq' (f : α →₁ₛ β) : ∥f∥ = ennreal.to_real (edist (f : α →ₘ β) 0) := rfl
id                        └─┘       └─────────────┘  └───┘      └┘         └─┘
src                        └─┘         └─────────────┘  └───┘        └┘          └─┘
typ                       └─┘       └─────────────┘  └───┘      └┘         └─┘
doc                        └─┘            └─────────────┘               └┘
489  
490  /-- Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
491    integral. -/
492  protected def normed_group : normed_group (α →₁ₛ β) :=
id                                └──────────┘   └─┘ 
src                               └──────────┘    └─┘
typ                               └──────────┘   └─┘ 
doc                               └──────────┘    └─┘
493  normed_group.of_add_dist (λ x, rfl) $ by
id   └──────────────────────┘      └─┘
src  └──────────────────────┘       └─┘
typ  └──────────────────────┘      └─┘
doc  └──────────────────────┘
st                                           
494    { intros, simp only [dist_eq, coe_add, l1.dist_eq, l1.coe_add], rw edist_eq_add_add }
id                          └─────┘  └─────┘  └────────┘  └────────┘      └──────────────┘
src      └────┘  └─────────┘└─────┘└┘└─────┘└┘└────────┘└┘└────────┘  └─┘└──────────────┘
typ      └────┘  └─────────┘└─────┘└┘└─────┘└┘└────────┘└┘└────────┘  └─┘└──────────────┘
doc      └────┘  └─────────┘       └┘       └┘          └┘            └─┘                
txt      └────┘  └─────────┘       └┘       └┘          └┘            └─┘                
par      └────┘  └─────────┘       └┘       └┘          └┘            └─┘                
pid                  └──┘└┘       └┘       └┘          └┘                              
st   ─────────┘└────────────────────────────────────────────────────┘└────────────────────┘└┘
495  
496  variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
id                          └──────────┘     └──────────┘
src                         └──────────┘     └──────────┘
typ                         └──────────┘     └──────────┘
doc                         └──────────┘     └──────────┘
497  
498  /-- Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
499    integral. -/
500  protected def has_scalar : has_scalar 𝕜 (α →₁ₛ β) := ⟨λk f, ⟨k • f,
id                              └────────┘    └─┘              
src                             └────────┘      └─┘                 
typ                             └────────┘    └─┘              
doc                             └────────┘      └─┘
501  begin
st   └─────
502    rcases f with ⟨f, ⟨s, hsi, hs⟩⟩,
id            
src    └─────┘ └─────────────────────┘
typ    └─────┘└─────────────────────┘
doc    └─────┘ └─────────────────────┘
txt    └─────┘ └─────────────────────┘
par    └─────┘ └─────────────────────┘
pid           └─────────────────────┘
st   ────────────────────────────────┘└─
503    use k • s, split,
id           
src    └──┘    └───┘
typ    └──┘  └───┘
doc    └──┘     └───┘
txt    └──┘     └───┘
par    └──┘     └───┘
pid         
st   ──────────┘└─────┘└─
504    { exact integrable.smul _ hsi },
id             └─────────────┘   └─┘
src      └────┘└─────────────┘└─┘   
typ      └────┘└─────────────┘└─┘└─┘
doc      └────┘               └─┘   
txt      └────┘               └─┘   
par      └────┘               └─┘   
pid                          └─┘   
st   ───┘└──────────────────────────┘└┘
505    { rw [coe_smul, subtype.coe_mk, ← hs], refl }
id           └──────┘  └────────────┘    └┘
src      └──┘└──────┘└┘└────────────┘└──┘    └───┘
typ      └──┘└──────┘└┘└────────────┘└──┘└┘  └───┘
doc      └──┘        └┘              └──┘    └───┘
txt      └──┘        └┘              └──┘    └───┘
par      └──┘        └┘              └──┘    └───┘
pid        └┘        └┘              └──┘        
st   ───────────────┘└──────────────┘└────┘└──────┘└─
506  end ⟩⟩
st   ──┘
507  
508  local attribute [instance, priority 10000] simple_func.has_scalar
id                                              └────────────────────┘
src                                             └────────────────────┘
typ                                             └────────────────────┘
doc                                             └────────────────────┘
509  
510  @[simp, move_cast] lemma coe_smul (c : 𝕜) (f : α →₁ₛ β) :
id                                                  └─┘ 
src                                                   └─┘
typ                                                 └─┘ 
doc    └──┘  └───────┘                                └─┘
511    ((c • f : α →₁ₛ β) : α →₁ β) = c • (f : α →₁ β) := rfl
id             └─┘      └┘           └┘      └─┘
src               └─┘        └┘               └┘       └─┘
typ            └─┘      └┘           └┘      └─┘
doc                └─┘        └┘                 └┘
512  
513  /-- Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
514    integral. -/
515  protected def semimodule : semimodule 𝕜 (α →₁ₛ β) :=
id                              └────────┘    └─┘ 
src                             └────────┘      └─┘
typ                             └────────┘    └─┘ 
doc                             └────────┘      └─┘
516  { one_smul  := λf, simple_func.eq (by { simp only [coe_smul], exact one_smul _ _ }),
id                     └────────────┘                  └──────┘         └──────┘
src                     └────────────┘       └─────────┘└──────┘  └────┘└──────┘└───┘
typ                    └────────────┘       └─────────┘└──────┘  └────┘└──────┘└───┘
doc                                          └─────────┘          └────┘        └───┘
txt                                          └─────────┘          └────┘        └───┘
par                                          └─────────┘          └────┘        └───┘
pid                                              └──┘└┘                       └──┘
st                                        └─────────────────────┘└───────────────────┘└┘
517    mul_smul  := λx y f, simple_func.eq (by { simp only [coe_smul], exact mul_smul _ _ _ }),
id                       └────────────┘                  └──────┘         └──────┘
src                         └────────────┘       └─────────┘└──────┘  └────┘└──────┘└─────┘
typ                      └────────────┘       └─────────┘└──────┘  └────┘└──────┘└─────┘
doc                                              └─────────┘          └────┘        └─────┘
txt                                              └─────────┘          └────┘        └─────┘
par                                              └─────────┘          └────┘        └─────┘
pid                                                  └──┘└┘                       └────┘
st                                            └─────────────────────┘└─────────────────────┘└┘
518    smul_add  := λx f g, simple_func.eq (by { simp only [coe_smul, coe_add], exact smul_add _ _ _ }),
id                       └────────────┘                  └──────┘  └─────┘         └──────┘
src                         └────────────┘       └─────────┘└──────┘└┘└─────┘  └────┘└──────┘└─────┘
typ                      └────────────┘       └─────────┘└──────┘└┘└─────┘  └────┘└──────┘└─────┘
doc                                              └─────────┘        └┘         └────┘        └─────┘
txt                                              └─────────┘        └┘         └────┘        └─────┘
par                                              └─────────┘        └┘         └────┘        └─────┘
pid                                                  └──┘└┘        └┘                      └────┘
st                                            └──────────────────────────────┘└─────────────────────┘└┘
519    smul_zero := λx, simple_func.eq (by { simp only [coe_zero, coe_smul], exact smul_zero _ }),
id                     └────────────┘                  └──────┘  └──────┘         └───────┘
src                     └────────────┘       └─────────┘└──────┘└┘└──────┘  └────┘└───────┘└─┘
typ                    └────────────┘       └─────────┘└──────┘└┘└──────┘  └────┘└───────┘└─┘
doc                                          └─────────┘        └┘          └────┘         └─┘
txt                                          └─────────┘        └┘          └────┘         └─┘
par                                          └─────────┘        └┘          └────┘         └─┘
pid                                              └──┘└┘        └┘                        └┘
st                                        └───────────────────────────────┘└──────────────────┘└┘
520    add_smul  := λx y f, simple_func.eq (by { simp only [coe_smul], exact add_smul _ _ _ }),
id                       └────────────┘                  └──────┘         └──────┘
src                         └────────────┘       └─────────┘└──────┘  └────┘└──────┘└─────┘
typ                      └────────────┘       └─────────┘└──────┘  └────┘└──────┘└─────┘
doc                                              └─────────┘          └────┘        └─────┘
txt                                              └─────────┘          └────┘        └─────┘
par                                              └─────────┘          └────┘        └─────┘
pid                                                  └──┘└┘                       └────┘
st                                            └─────────────────────┘└─────────────────────┘└┘
521    zero_smul := λf, simple_func.eq (by { simp only [coe_smul], exact zero_smul _ _ }) }
id                     └────────────┘                  └──────┘         └───────┘
src                     └────────────┘       └─────────┘└──────┘  └────┘└───────┘└───┘
typ                    └────────────┘       └─────────┘└──────┘  └────┘└───────┘└───┘
doc                                          └─────────┘          └────┘         └───┘
txt                                          └─────────┘          └────┘         └───┘
par                                          └─────────┘          └────┘         └───┘
pid                                              └──┘└┘                        └──┘
st                                        └─────────────────────┘└────────────────────┘└┘
522  
523  /-- Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
524    integral. -/
525  protected def module : module 𝕜 (α →₁ₛ β) :=
id                          └────┘    └─┘ 
src                         └────┘      └─┘
typ                         └────┘    └─┘ 
doc                         └────┘      └─┘
526  { .. simple_func.semimodule }
id        └────────────────────┘
src       └────────────────────┘
typ       └────────────────────┘
doc       └────────────────────┘
527  
528  /-- Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
529    integral. -/
530  protected def vector_space : vector_space 𝕜 (α →₁ₛ β) :=
id                                └──────────┘    └─┘ 
src                               └──────────┘      └─┘
typ                               └──────────┘    └─┘ 
doc                               └──────────┘      └─┘
531  { .. simple_func.semimodule }
id        └────────────────────┘
src       └────────────────────┘
typ       └────────────────────┘
doc       └────────────────────┘
532  
533  local attribute [instance] simple_func.vector_space simple_func.normed_group
id                              └──────────────────────┘ └──────────────────────┘
src                             └──────────────────────┘ └──────────────────────┘
typ                             └──────────────────────┘ └──────────────────────┘
doc                             └──────────────────────┘ └──────────────────────┘
534  
535  /-- Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
536    integral. -/
537  protected def normed_space : normed_space 𝕜 (α →₁ₛ β) :=
id                                └──────────┘    └─┘ 
src                               └──────────┘      └─┘
typ                               └──────────┘    └─┘ 
doc                               └──────────┘      └─┘
538  ⟨ λc f, by { rw [norm_eq, norm_eq, coe_smul, norm_smul] } ⟩
id                  └─────┘  └─────┘  └──────┘  └───────┘
src               └──┘└─────┘└┘└─────┘└┘└──────┘└┘└───────┘└┘
typ             └──┘└─────┘└┘└─────┘└┘└──────┘└┘└───────┘└┘
doc               └──┘       └┘       └┘        └┘         └┘
txt               └──┘       └┘       └┘        └┘         └┘
par               └──┘       └┘       └┘        └┘         └┘
pid                 └┘       └┘       └┘        └┘         
st             └────────────┘└───────┘└────────┘└─────────┘└┘
539  
540  end instances
541  
542  local attribute [instance] simple_func.normed_group simple_func.normed_space
id                              └──────────────────────┘ └──────────────────────┘
src                             └──────────────────────┘ └──────────────────────┘
typ                             └──────────────────────┘ └──────────────────────┘
doc                             └──────────────────────┘ └──────────────────────┘
543  
544  section of_simple_func
545  
546  /-- Construct the equivalence class `[f]` of an integrable simple function `f`. -/
547  @[reducible] def of_simple_func (f : α →ₛ β) (hf : integrable f) : (α →₁ₛ β) :=
id                                         └┘         └────────┘       └─┘ 
src                                         └┘          └────────┘         └─┘
typ                                        └┘         └────────┘       └─┘ 
doc    └───────┘                            └┘          └────────┘         └─┘
548    ⟨l1.of_fun f f.measurable hf, ⟨f, ⟨hf, rfl⟩⟩⟩
id      └───────┘  └─────────┘ └┘      └┘  └─┘
src     └───────┘    └─────────┘              └─┘
typ     └───────┘  └─────────┘ └┘      └┘  └─┘
doc     └───────┘    └─────────┘
549  
550  lemma of_simple_func_eq_of_fun (f : α →ₛ β) (hf : integrable f) :
id                                        └┘         └────────┘ 
src                                        └┘          └────────┘
typ                                       └┘         └────────┘ 
doc                                        └┘          └────────┘
551    (of_simple_func f hf : α →₁ β) = l1.of_fun f f.measurable hf := rfl
id      └────────────┘  └┘    └┘    └───────┘  └─────────┘ └┘    └─┘
src     └────────────┘          └┘     └───────┘    └─────────┘       └─┘
typ     └────────────┘  └┘    └┘    └───────┘  └─────────┘ └┘    └─┘
doc     └────────────┘          └┘      └───────┘    └─────────┘
552  
553  lemma of_simple_func_eq_mk (f : α →ₛ β) (hf : integrable f) :
id                                    └┘         └────────┘ 
src                                    └┘          └────────┘
typ                                   └┘         └────────┘ 
doc                                    └┘          └────────┘
554    (of_simple_func f hf : α →ₘ β) = ae_eq_fun.mk f f.measurable := rfl
id      └────────────┘  └┘    └┘    └──────────┘  └─────────┘    └─┘
src     └────────────┘          └┘     └──────────┘    └─────────┘    └─┘
typ     └────────────┘  └┘    └┘    └──────────┘  └─────────┘    └─┘
doc     └────────────┘          └┘      └──────────┘    └─────────┘
555  
556  lemma of_simple_func_zero : of_simple_func (0 : α →ₛ β) (integrable_zero α β) = 0 := rfl
id                               └────────────┘       └┘    └─────────────┘          └─┘
src                              └────────────┘        └┘     └─────────────┘            └─┘
typ                              └────────────┘       └┘    └─────────────┘          └─┘
doc                              └────────────┘        └┘
557  
558  lemma of_simple_func_add (f g : α →ₛ β) (hf hg) :
id                                    └┘ 
src                                    └┘
typ                                   └┘ 
doc                                    └┘
559    of_simple_func (f + g) (integrable.add f.measurable hf g.measurable hg) = of_simple_func f hf +
id     └────────────┘       └────────────┘ └─────────┘ └┘ └─────────┘ └┘   └────────────┘  └┘ 
src    └────────────┘         └────────────┘  └─────────┘     └─────────┘      └────────────┘      
typ    └────────────┘       └────────────┘ └─────────┘ └┘ └─────────┘ └┘   └────────────┘  └┘ 
doc    └────────────┘                          └─────────┘     └─────────┘       └────────────┘
560      of_simple_func g hg := rfl
id       └────────────┘  └┘    └─┘
src      └────────────┘         └─┘
typ      └────────────┘  └┘    └─┘
doc      └────────────┘
561  
562  lemma of_simple_func_neg (f : α →ₛ β) (hf) :
id                                  └┘ 
src                                  └┘
typ                                 └┘ 
doc                                  └┘
563    of_simple_func (-f) (integrable.neg hf) = -of_simple_func f hf := rfl
id     └────────────┘     └────────────┘ └┘   └────────────┘  └┘    └─┘
src    └────────────┘      └────────────┘      └────────────┘         └─┘
typ    └────────────┘     └────────────┘ └┘   └────────────┘  └┘    └─┘
doc    └────────────┘                             └────────────┘
564  
565  lemma of_simple_func_sub (f g : α →ₛ β) (hf hg) :
id                                    └┘ 
src                                    └┘
typ                                   └┘ 
doc                                    └┘
566    of_simple_func (f - g) (integrable.sub f.measurable hf g.measurable hg) = of_simple_func f hf -
id     └────────────┘       └────────────┘ └─────────┘ └┘ └─────────┘ └┘   └────────────┘  └┘ 
src    └────────────┘         └────────────┘  └─────────┘     └─────────┘      └────────────┘      
typ    └────────────┘       └────────────┘ └─────────┘ └┘ └─────────┘ └┘   └────────────┘  └┘ 
doc    └────────────┘                          └─────────┘     └─────────┘       └────────────┘
567      of_simple_func g hg := rfl
id       └────────────┘  └┘    └─┘
src      └────────────┘         └─┘
typ      └────────────┘  └┘    └─┘
doc      └────────────┘
568  
569  variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
id                          └──────────┘     └──────────┘
src                         └──────────┘     └──────────┘
typ                         └──────────┘     └──────────┘
doc                         └──────────┘     └──────────┘
570  
571  lemma of_simple_func_smul (f : α →ₛ β) (hf) (c : 𝕜) :
id                                   └┘             
src                                   └┘
typ                                  └┘             
doc                                   └┘
572    of_simple_func (c • f) (integrable.smul _ hf) = c • of_simple_func f hf := rfl
id     └────────────┘       └─────────────┘   └┘     └────────────┘  └┘    └─┘
src    └────────────┘         └─────────────┘           └────────────┘         └─┘
typ    └────────────┘       └─────────────┘   └┘     └────────────┘  └┘    └─┘
doc    └────────────┘                                      └────────────┘
573  
574  lemma norm_of_simple_func (f : α →ₛ β) (hf) : ∥of_simple_func f hf∥ = ennreal.to_real (∫⁻ a, edist (f a) 0) :=
id                                   └┘          └────────────┘  └┘  └─────────────┘  └┘  └───┘   
src                                   └┘           └────────────┘       └─────────────┘  └┘   └───┘
typ                                  └┘          └────────────┘  └┘  └─────────────┘  └┘  └───┘   
doc                                   └┘            └────────────┘         └─────────────┘  └┘  
575  rfl
id   └─┘
src  └─┘
typ  └─┘
576  
577  end of_simple_func
578  
579  section to_simple_func
580  
581  /-- Find a representative of a `l1.simple_func`. -/
582  def to_simple_func (f : α →₁ₛ β) : α →ₛ β := classical.some f.2
id                            └─┘      └┘     └────────────┘ 
src                            └─┘        └┘      └────────────┘  
typ                           └─┘      └┘     └────────────┘ 
doc                            └─┘        └┘
583  
584  /-- `f.to_simple_func` is measurable. -/
585  protected lemma measurable (f : α →₁ₛ β) : measurable f.to_simple_func := f.to_simple_func.measurable
id                                    └─┘     └────────┘ └─────────────┘    └─────────────┘└─────────┘
src                                    └─┘      └────────┘  └─────────────┘     └─────────────┘└─────────┘
typ                                   └─┘     └────────┘ └─────────────┘    └─────────────┘└─────────┘
doc                                    └─┘      └────────┘  └─────────────┘     └─────────────┘└─────────┘
586  
587  /-- `f.to_simple_func` is integrable. -/
588  protected lemma integrable (f : α →₁ₛ β) : integrable f.to_simple_func :=
id                                    └─┘     └────────┘ └─────────────┘
src                                    └─┘      └────────┘  └─────────────┘
typ                                   └─┘     └────────┘ └─────────────┘
doc                                    └─┘      └────────┘  └─────────────┘
589  let ⟨h, _⟩ := classical.some_spec f.2 in h
id   └─┘          └─────────────────┘ 
src                └─────────────────┘  
typ  └─┘          └─────────────────┘ 
590  
591  lemma of_simple_func_to_simple_func (f : α →₁ₛ β) :
id                                             └─┘ 
src                                             └─┘
typ                                            └─┘ 
doc                                             └─┘
592    of_simple_func (f.to_simple_func) f.integrable = f :=
id     └────────────┘  └─────────────┘  └─────────┘  
src    └────────────┘   └─────────────┘   └─────────┘ 
typ    └────────────┘  └─────────────┘  └─────────┘  
doc    └────────────┘   └─────────────┘   └─────────┘
593  by { rw ← simple_func.eq_iff', exact (classical.some_spec f.2).2 }
id             └─────────────────┘         └─────────────────┘ 
src       └───┘└─────────────────┘  └────┘ └─────────────────┘ └────┘
typ       └───┘└─────────────────┘  └────┘ └─────────────────┘└────┘
doc       └───┘                     └────┘                     └────┘
txt       └───┘                     └────┘                     └────┘
par       └───┘                     └────┘                     └────┘
pid         └─┘                                               └─┘└─┘
st     └─────────────────────────┘└──────────────────────────────────┘└┘
594  
595  lemma to_simple_func_of_simple_func (f : α →ₛ β) (hfi) :
id                                             └┘ 
src                                             └┘
typ                                            └┘ 
doc                                             └┘
596    ∀ₘ a, (of_simple_func f hfi).to_simple_func a = f a :=
id     └┘   └────────────┘  └─┘ └────────────┘     
src    └┘    └────────────┘       └────────────┘    
typ    └┘   └────────────┘  └─┘ └────────────┘     
doc    └┘    └────────────┘       └────────────┘
597  by { rw ← mk_eq_mk, exact (classical.some_spec (of_simple_func f hfi).2).2 }
id             └──────┘         └─────────────────┘  └────────────┘  └─┘
src       └───┘└──────┘  └────┘ └─────────────────┘ └────────────┘    └─────┘
typ       └───┘└──────┘  └────┘ └─────────────────┘ └────────────┘└─┘└─────┘
doc       └───┘          └────┘                     └────────────┘    └─────┘
txt       └───┘          └────┘                                       └─────┘
par       └───┘          └────┘                                       └─────┘
pid         └─┘                                                      └──┘└─┘
st     └──────────────┘└───────────────────────────────────────────────────────┘└┘
598  
599  lemma to_simple_func_eq_to_fun (f : α →₁ₛ β) : ∀ₘ a, (f.to_simple_func) a = (f : α →₁ β).to_fun a :=
id                                        └─┘     └┘   └─────────────┘         └┘  └────┘  
src                                        └─┘      └┘     └─────────────┘            └┘   └────┘
typ                                       └─┘     └┘   └─────────────┘         └┘  └────┘  
doc                                        └─┘      └┘     └─────────────┘             └┘   └────┘
600  begin
st   └─────
601    rw [← of_fun_eq_of_fun (f.to_simple_func) (f : α →₁ β).to_fun f.measurable f.integrable
id           └──────────────┘  └──────────────┘         └┘           └──────────┘ └──────────┘
src    └────┘└──────────────┘ └──────────────┘└┘  └─┘ └┘ └───────┘└──────────┘└──────────┘
typ    └────┘└──────────────┘ └──────────────┘└┘  └─┘ └┘ └───────┘└──────────┘└──────────┘
doc    └────┘                 └──────────────┘└┘  └─┘ └┘ └───────┘└──────────┘└──────────┘
txt    └────┘                                 └┘  └─┘    └───────┘                        
par    └────┘                                 └┘  └─┘    └───────┘                        
pid      └──┘                                 └┘  └─┘    └───────┘                        
st   ──────────────────────────────────────────────────────────────────────────────────────────
602      (f:α→₁β).measurable (f:α→₁β).integrable, ← l1.eq_iff],
id                                               └───────┘
src  ───┘      └───────────┘      └──────────────┘└───────┘
typ  ───┘      └───────────┘   └──────────────┘└───────┘
doc  ───┘      └───────────┘      └──────────────┘         
txt  ───┘      └───────────┘      └──────────────┘         
par  ───┘      └───────────┘      └──────────────┘         
pid  ───┘      └───────────┘      └──────────────┘         
st   ─────────────────────────────────────────┘└────────────┘└──
603    simp only [of_fun_eq_mk],
id                └──────────┘
src    └─────────┘└──────────┘
typ    └─────────┘└──────────┘
doc    └─────────┘            
txt    └─────────┘            
par    └─────────┘            
pid        └──┘└┘            
st   ─────────────────────────┘└─
604    rcases classical.some_spec f.2 with ⟨_, h⟩, convert h, rw mk_to_fun, refl
id            └─────────────────┘                              └───────┘
src    └─────┘└─────────────────┘ └────────────┘  └──────┘   └─┘└───────┘  └───┘
typ    └─────┘└─────────────────┘└────────────┘  └──────┘  └─┘└───────┘  └───┘
doc    └─────┘                    └────────────┘  └──────┘   └─┘           └───┘
txt    └─────┘                    └────────────┘  └──────┘   └─┘           └───┘
par    └─────┘                    └────────────┘  └──────┘   └─┘           └───┘
pid                              └────────────┘                             
st   ───────────────────────────────────────────┘└─────────┘└────────────┘└─────┘
605  end
st   └─┘
606  
607  variables (α β)
608  lemma zero_to_simple_func : ∀ₘ a, (0 : α →₁ₛ β).to_simple_func a = 0 :=
id                               └┘        └─┘  └────────────┘   
src                              └┘          └─┘   └────────────┘    
typ                              └┘        └─┘  └────────────┘   
doc                              └┘          └─┘   └────────────┘
609  begin
st   └─────
610    filter_upwards [to_simple_func_eq_to_fun (0 : α →₁ₛ β), l1.zero_to_fun α β],
id                     └──────────────────────┘       └─┘    └────────────┘  
src    └──────────────┘└──────────────────────┘ └──┘ └─┘ └─┘└────────────┘  
typ    └──────────────┘└──────────────────────┘ └──┘└─┘└─┘└────────────┘
doc    └──────────────┘                         └──┘ └─┘ └─┘                
txt    └──────────────┘                         └──┘     └─┘                
par    └──────────────┘                         └──┘     └─┘                
pid                  └┘                         └──┘     └─┘                
st   ────────────────────────────────────────────────────────────────────────────┘└─
611    assume a,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
612    simp only [mem_set_of_eq],
id                └───────────┘
src    └─────────┘└───────────┘
typ    └─────────┘└───────────┘
doc    └─────────┘             
txt    └─────────┘             
par    └─────────┘             
pid        └──┘└┘             
st   ──────────────────────────┘└─
613    assume h,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
614    rw h,
id        
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ─────┘└─
615    assume h,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
616    exact h
id           
src    └────┘ 
typ    └────┘
doc    └────┘ 
txt    └────┘ 
par    └────┘ 
pid          
st   ─────────┘
617  end
st   └─┘
618  variables {α β}
619  
620  lemma add_to_simple_func (f g : α →₁ₛ β) :
id                                    └─┘ 
src                                    └─┘
typ                                   └─┘ 
doc                                    └─┘
621    ∀ₘ a, (f + g).to_simple_func a = f.to_simple_func a + g.to_simple_func a :=
id     └┘      └────────────┘    └─────────────┘   └─────────────┘ 
src    └┘         └────────────┘      └─────────────┘     └─────────────┘
typ    └┘      └────────────┘    └─────────────┘   └─────────────┘ 
doc    └┘          └────────────┘       └─────────────┘      └─────────────┘
622  begin
st   └─────
623    filter_upwards [to_simple_func_eq_to_fun (f + g), to_simple_func_eq_to_fun f,
id                     └──────────────────────┘       └──────────────────────┘ 
src    └──────────────┘└──────────────────────┘   └─┘└──────────────────────┘ └─
typ    └──────────────┘└──────────────────────┘ └─┘└──────────────────────┘└─
doc    └──────────────┘                            └─┘                         └─
txt    └──────────────┘                            └─┘                         └─
par    └──────────────┘                            └─┘                         └─
pid                  └┘                            └─┘                         └─
st   ────────────────────────────────────────────────────────────────────────────────
624      to_simple_func_eq_to_fun g, l1.add_to_fun (f:α→₁β) g],
id       └──────────────────────┘   └───────────┘   └┘  
src  ───┘└──────────────────────┘ └┘└───────────┘   └┘ └┘ 
typ  ───┘└──────────────────────┘└┘└───────────┘ └┘└┘
doc  ───┘                         └┘                └┘ └┘ 
txt  ───┘                         └┘                   └┘ 
par  ───┘                         └┘                   └┘ 
pid  ───┘                         └┘                   └┘ 
st   ────────────────────────────────────────────────────────┘└─
625    assume a,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
626    simp only [mem_set_of_eq],
id                └───────────┘
src    └─────────┘└───────────┘
typ    └─────────┘└───────────┘
doc    └─────────┘             
txt    └─────────┘             
par    └─────────┘             
pid        └──┘└┘             
st   ──────────────────────────┘└─
627    repeat { assume h, rw h },
id                           
src    └───────┘└──────┘└┘└─┘ 
typ    └───────┘└──────┘└┘└─┘
doc    └───────┘└──────┘└┘└─┘ 
txt    └───────┘└──────┘└┘└─┘ 
par    └───────┘└──────┘└┘└─┘ 
pid          └──────────────┘ └┘
st   ──────────────────┘└─────┘└┘
628    assume h,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
629    rw ← h,
id          
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ───────┘└─
630    refl
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
631  end
st   └─┘
632  
633  lemma neg_to_simple_func (f : α →₁ₛ β) : ∀ₘ a, (-f).to_simple_func a = - f.to_simple_func a :=
id                                  └─┘     └┘    └────────────┘     └─────────────┘ 
src                                  └─┘      └┘      └────────────┘       └─────────────┘
typ                                 └─┘     └┘    └────────────┘     └─────────────┘ 
doc                                  └─┘      └┘       └────────────┘         └─────────────┘
634  begin
st   └─────
635    filter_upwards [to_simple_func_eq_to_fun (-f), to_simple_func_eq_to_fun f, l1.neg_to_fun (f:α→₁β)],
id                     └──────────────────────┘     └──────────────────────┘   └───────────┘   └┘
src    └──────────────┘└──────────────────────┘  └─┘└──────────────────────┘ └┘└───────────┘   └┘ └┘
typ    └──────────────┘└──────────────────────┘ └─┘└──────────────────────┘└┘└───────────┘ └┘└┘
doc    └──────────────┘                           └─┘                         └┘                └┘ └┘
txt    └──────────────┘                           └─┘                         └┘                   └┘
par    └──────────────┘                           └─┘                         └┘                   └┘
pid                  └┘                           └─┘                         └┘                   └┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────────┘└─
636    assume a,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
637    simp only [mem_set_of_eq],
id                └───────────┘
src    └─────────┘└───────────┘
typ    └─────────┘└───────────┘
doc    └─────────┘             
txt    └─────────┘             
par    └─────────┘             
pid        └──┘└┘             
st   ──────────────────────────┘└─
638    repeat { assume h, rw h },
id                           
src    └───────┘└──────┘└┘└─┘ 
typ    └───────┘└──────┘└┘└─┘
doc    └───────┘└──────┘└┘└─┘ 
txt    └───────┘└──────┘└┘└─┘ 
par    └───────┘└──────┘└┘└─┘ 
pid          └──────────────┘ └┘
st   ──────────────────┘└─────┘└┘
639    assume h,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
640    rw ← h,
id          
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ───────┘└─
641    refl
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
642  end
st   └─┘
643  
644  lemma sub_to_simple_func (f g : α →₁ₛ β) :
id                                    └─┘ 
src                                    └─┘
typ                                   └─┘ 
doc                                    └─┘
645    ∀ₘ a, (f - g).to_simple_func a = f.to_simple_func a - g.to_simple_func a :=
id     └┘      └────────────┘    └─────────────┘   └─────────────┘ 
src    └┘         └────────────┘      └─────────────┘     └─────────────┘
typ    └┘      └────────────┘    └─────────────┘   └─────────────┘ 
doc    └┘          └────────────┘       └─────────────┘      └─────────────┘
646  begin
st   └─────
647    filter_upwards [to_simple_func_eq_to_fun (f - g), to_simple_func_eq_to_fun f,
id                     └──────────────────────┘       └──────────────────────┘ 
src    └──────────────┘└──────────────────────┘   └─┘└──────────────────────┘ └─
typ    └──────────────┘└──────────────────────┘ └─┘└──────────────────────┘└─
doc    └──────────────┘                            └─┘                         └─
txt    └──────────────┘                            └─┘                         └─
par    └──────────────┘                            └─┘                         └─
pid                  └┘                            └─┘                         └─
st   ────────────────────────────────────────────────────────────────────────────────
648      to_simple_func_eq_to_fun g, l1.sub_to_fun (f:α→₁β) g],
id       └──────────────────────┘   └───────────┘   └┘  
src  ───┘└──────────────────────┘ └┘└───────────┘   └┘ └┘ 
typ  ───┘└──────────────────────┘└┘└───────────┘ └┘└┘
doc  ───┘                         └┘                └┘ └┘ 
txt  ───┘                         └┘                   └┘ 
par  ───┘                         └┘                   └┘ 
pid  ───┘                         └┘                   └┘ 
st   ────────────────────────────────────────────────────────┘
649    assume a,
650    simp only [mem_set_of_eq],
651    repeat { assume h, rw h },
652    assume h,
653    rw ← h,
654    refl
655  end
st   └─┘
656  
657  variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
id                          └──────────┘     └──────────┘
src                         └──────────┘     └──────────┘
typ                         └──────────┘     └──────────┘
doc                         └──────────┘     └──────────┘
658  
659  lemma smul_to_simple_func (k : 𝕜) (f : α →₁ₛ β) :
id                                          └─┘ 
src                                           └─┘
typ                                         └─┘ 
doc                                           └─┘
660    ∀ₘ a, (k • f).to_simple_func a = k • f.to_simple_func a :=
id     └┘      └────────────┘      └─────────────┘ 
src    └┘         └────────────┘         └─────────────┘
typ    └┘      └────────────┘      └─────────────┘ 
doc    └┘          └────────────┘           └─────────────┘
661  begin
662    filter_upwards [to_simple_func_eq_to_fun (k • f), to_simple_func_eq_to_fun f,
663      l1.smul_to_fun k (f:α→₁β)],
664    assume a,
665    simp only [mem_set_of_eq],
666    repeat { assume h, rw h },
667    assume h,
668    rw ← h,
669    refl
670  end
st   └─┘
671  
672  lemma lintegral_edist_to_simple_func_lt_top (f g : α →₁ₛ β) :
id                                                           
typ                                                          
673    (∫⁻ (x : α), edist ((to_simple_func f) x) ((to_simple_func g) x)) < ⊤ :=
id                                                                 
typ                                                                
674  begin
675    rw lintegral_rw₂ (to_simple_func_eq_to_fun f) (to_simple_func_eq_to_fun g),
676    exact lintegral_edist_to_fun_lt_top _ _
677  end
st   └─┘
678  
679  lemma dist_to_simple_func (f g : α →₁ₛ β) : dist f g =
id                                         
typ                                        
680    ennreal.to_real (∫⁻ x, edist (f.to_simple_func x) (g.to_simple_func x)) :=
id     └┘  └┘  └┘  └┘                                                    
src    └┘  └┘  └┘  └┘
typ    └┘  └┘  └┘  └┘                                                    
doc    └┘  └┘  └┘  └┘
681  begin
682    rw [dist_eq, l1.dist_to_fun, ennreal.to_real_eq_to_real],
683    { rw lintegral_rw₂, repeat { exact all_ae_eq_symm (to_simple_func_eq_to_fun _) } },
st                                                                                    └──┘
684    { exact l1.lintegral_edist_to_fun_lt_top _ _ },
st                                                  └┘
685    { exact lintegral_edist_to_simple_func_lt_top _ _ }
st                                                       └─
686  end
st   ──┘
687  
688  lemma norm_to_simple_func (f : α →₁ₛ β) :
id                                       
typ                                      
689    ∥f∥ = ennreal.to_real (∫⁻ (a : α), nnnorm ((to_simple_func f) a)) :=
id           └┘  └┘  └┘  └┘                                         
src          └┘  └┘  └┘  └┘
typ          └┘  └┘  └┘  └┘                                         
doc          └┘  └┘  └┘  └┘
690  calc ∥f∥ = ennreal.to_real (∫⁻x, edist (f.to_simple_func x) ((0 : α →₁ₛ β).to_simple_func x)) :
id              └┘ └┘  └┘  └┘                                                               
src             └┘ └┘  └┘  └┘
typ             └┘ └┘  └┘  └┘                                                               
doc             └┘ └┘  └┘  └┘
691  begin
692    rw [← dist_zero_right, dist_to_simple_func]
st                                               
693  end
st   └─┘
694  ... = ennreal.to_real (∫⁻ (x : α), (coe ∘ nnnorm) (f.to_simple_func x)) :
id         └─────────────┘                                              
src        └─────────────┘
typ        └─────────────┘                                              
doc        └─────────────┘
695  begin
696    rw lintegral_nnnorm_eq_lintegral_edist,
697    have : (∫⁻ (x : α), edist ((to_simple_func f) x) ((to_simple_func (0:α→₁ₛβ)) x)) =
id                                                                              
typ                                                                             
698              ∫⁻ (x : α), edist ((to_simple_func f) x) 0,
id                       
typ                      
699    { apply lintegral_congr_ae, filter_upwards [zero_to_simple_func α β],
id                                                                      
typ                                                                     
700      assume a,
701      simp only [mem_set_of_eq],
702      assume h,
703      rw h },
st            └┘
704    rw [ennreal.to_real_eq_to_real],
705    { exact this },
st                  └┘
706    { exact lintegral_edist_to_simple_func_lt_top _ _ },
st                                                       └┘
707    { rw ← this, exact lintegral_edist_to_simple_func_lt_top _ _ }
st                                                                  └─
708  end
st   ──┘
709  
710  lemma norm_eq_bintegral (f : α →₁ₛ β) : ∥f∥ = (f.to_simple_func.map norm).bintegral :=
id                                     
typ                                    
711  calc ∥f∥ = ennreal.to_real (∫⁻ (x : α), (coe ∘ nnnorm) (f.to_simple_func x)) :
id              └┘  └┘  └┘  └┘                                               
src             └┘  └┘  └┘  └┘
typ             └┘  └┘  └┘  └┘                                               
doc             └┘  └┘  └┘  └┘
712    by { rw norm_to_simple_func }
st                                 └┘
713  ... = (f.to_simple_func.map norm).bintegral :
714  begin
715    rw ← f.to_simple_func.bintegral_eq_lintegral (coe ∘ nnnorm) f.integrable,
716    { congr },
st             └┘
717    { simp only [nnnorm_zero, function.comp_app, ennreal.coe_zero] },
st                                                                    └┘
718    { assume b, exact coe_lt_top }
st                                  └─
719  end
st   ──┘
720  
721  end to_simple_func
722  
723  section coe_to_l1
724  /-! The embedding of integrable simple functions `α →₁ₛ β` into L1 is a uniform and dense embedding. -/
725  
726  lemma exists_simple_func_near (f : α →₁ β) {ε : ℝ} (ε0 : 0 < ε) :
id                                                             
src                                                  
typ                                                            
727    ∃ s : α →₁ₛ β, dist f s < ε :=
id                             
typ                            
728  begin
729    rcases f with ⟨⟨f, hfm⟩, hfi⟩,
730    simp only [integrable_mk, quot_mk_eq_mk] at hfi,
731    rcases simple_func_sequence_tendsto' hfm hfi with ⟨F, ⟨h₁, h₂⟩⟩,
732    rw ennreal.tendsto_at_top at h₂,
733    rcases h₂ (ennreal.of_real (ε/2)) (of_real_pos.2 $ half_pos ε0) with ⟨N, hN⟩,
id                └─────────────┘  
src               └─────────────┘
typ               └─────────────┘  
doc               └─────────────┘
734    have : (∫⁻ (x : α), nndist (F N x) (f x)) < ennreal.of_real ε :=
id                                              └─────────────┘ 
src                                                └─────────────┘
typ                                             └─────────────┘ 
doc                                                └─────────────┘
735      calc (∫⁻ (x : α), nndist (F N x) (f x)) ≤ 0 + ennreal.of_real (ε/2) : (hN N (le_refl _)).2
id                                                                               
typ                                                                              
736      ... < ennreal.of_real ε :
id             └─────────────┘ 
src            └─────────────┘
typ            └─────────────┘ 
doc            └─────────────┘
737        by { simp only [zero_add, of_real_lt_of_real_iff ε0], exact half_lt_self ε0 },
st                                                                                     └┘
738    { refine ⟨of_simple_func (F N) (h₁ N), _⟩, rw dist_comm,
id                                        
typ                                       
739      rw lt_of_real_iff_to_real_lt _ at this,
740      { simpa [edist_mk_mk', of_simple_func, l1.of_fun, l1.dist_eq] },
st                                                                     └┘
741      rw ← lt_top_iff_ne_top, exact lt_trans this (by simp [lt_top_iff_ne_top, of_real_ne_top]) },
st                                                                                                 └┘
742    { exact zero_ne_top }
st                         └─
743  end
st   ──┘
744  
745  protected lemma uniform_continuous : uniform_continuous (coe : (α →₁ₛ β) → (α →₁ β)) :=
id                                                                                 
typ                                                                                
746  uniform_continuous_comap
747  
748  protected lemma uniform_embedding : uniform_embedding (coe : (α →₁ₛ β) → (α →₁ β)) :=
id                                                                               
typ                                                                              
749  uniform_embedding_comap subtype.val_injective
750  
751  protected lemma uniform_inducing : uniform_inducing (coe : (α →₁ₛ β) → (α →₁ β)) :=
id                                                                             
typ                                                                            
752  simple_func.uniform_embedding.to_uniform_inducing
753  
754  protected lemma dense_embedding : dense_embedding (coe : (α →₁ₛ β) → (α →₁ β)) :=
id                                                                           
typ                                                                          
755  simple_func.uniform_embedding.dense_embedding $
756  λ f, mem_closure_iff_nhds.2 $ λ t ht,
757  let ⟨ε,ε0, hε⟩ := metric.mem_nhds_iff.1 ht in
758  let ⟨s, h⟩ := exists_simple_func_near f ε0 in
759  ⟨_, hε (metric.mem_ball'.2 h), s, rfl⟩
760  
761  protected lemma dense_inducing : dense_inducing (coe : (α →₁ₛ β) → (α →₁ β)) :=
id                                                                         
typ                                                                        
762  simple_func.dense_embedding.to_dense_inducing
763  
764  protected lemma dense_range : dense_range (coe : (α →₁ₛ β) → (α →₁ β)) :=
id                                                                   
typ                                                                  
765  simple_func.dense_inducing.dense
766  
767  variables (𝕜 : Type*) [normed_field 𝕜] [normed_space 𝕜 β]
id                                
src                               
typ                               
doc                               
768  
769  variables (α β)
770  
771  /-- The uniform and dense embedding of L1 simple functions into L1 functions. -/
772  def coe_to_l1 : (α →₁ₛ β) →L[𝕜] (α →₁ β) :=
id                                     
typ                                    
773  { to_fun := (coe : (α →₁ₛ β) → (α →₁ β)),
id                                     
typ                                    
774    add := λf g, rfl,
775    smul := λk f, rfl,
id              
typ             
776    cont := l1.simple_func.uniform_continuous.continuous, }
777  
778  variables {α β 𝕜}
779  
780  end coe_to_l1
781  
782  section pos_part
783  
784  /-- Positive part of a simple function in L1 space.  -/
785  def pos_part (f : α →₁ₛ ℝ) : α →₁ₛ ℝ := ⟨l1.pos_part (f : α →₁ ℝ),
id                                                             
src                                                               
typ                                                            
786  begin
787    rcases f with ⟨f, s, hsi, hsf⟩,
788    use s.pos_part,
789    split,
790    { exact integrable.max_zero hsi },
st                                     └┘
791    { simp only [subtype.coe_mk],
792      rw [l1.coe_pos_part, ← hsf, ae_eq_fun.pos_part, ae_eq_fun.zero_def, comp₂_mk_mk, mk_eq_mk],
793      filter_upwards [],
794      simp only [mem_set_of_eq],
795      assume a,
796      refl }
st            └─
797  end ⟩
st   ──┘
798  
799  /-- Negative part of a simple function in L1 space. -/
800  def neg_part (f : α →₁ₛ ℝ) : α →₁ₛ ℝ := pos_part (-f)
id                                   
src                                    
typ                                  
801  
802  @[move_cast] lemma coe_pos_part (f : α →₁ₛ ℝ) : (f.pos_part : α →₁ ℝ) = (f : α →₁ ℝ).pos_part := rfl
id                                                                                
src                                                                                  
typ                                                                               
doc    └───────┘
803  
804  @[move_cast] lemma coe_neg_part (f : α →₁ₛ ℝ) : (f.neg_part : α →₁ ℝ) = (f : α →₁ ℝ).neg_part := rfl
id                                                                                
src                                                                                  
typ                                                                               
doc    └───────┘
805  
806  end pos_part
807  
808  section simple_func_integral
809  /-! Define the Bochner integral on `α →₁ₛ β` and prove basic properties of this integral. -/
810  
811  variables [normed_space ℝ β]
id                           
src                          
typ                          
812  
813  /-- The Bochner integral over simple functions in l1 space. -/
814  def integral (f : α →₁ₛ β) : β := (f.to_simple_func).bintegral
id                              
typ                             
815  
816  lemma integral_eq_bintegral (f : α →₁ₛ β) : integral f = (f.to_simple_func).bintegral := rfl
id                                         
typ                                        
817  
818  lemma integral_eq_lintegral {f : α →₁ₛ ℝ} (h_pos : ∀ₘ a, 0 ≤ f.to_simple_func a) :
id                                                                              
src                                         
typ                                                                             
819    integral f = ennreal.to_real (∫⁻ a, ennreal.of_real (f.to_simple_func a)) :=
id                  └┘  └┘  └┘  └┘        └┘  └┘  └┘  └┘                    
src                 └┘  └┘  └┘  └┘         └┘  └┘  └┘  └┘
typ                 └┘  └┘  └┘  └┘        └┘  └┘  └┘  └┘                    
doc                 └┘  └┘  └┘  └┘         └┘  └┘  └┘  └┘
820  by { rw [integral, simple_func.bintegral_eq_lintegral' f.integrable h_pos], refl }
st                                                                                    └┘
821  
822  lemma integral_congr (f g : α →₁ₛ β) (h : ∀ₘ a, f.to_simple_func a = g.to_simple_func a) :
id                                                                                     
typ                                                                                    
823    integral f = integral g :=
824  by { simp only [integral], apply simple_func.bintegral_congr f.integrable g.integrable, exact h }
st                                                                                                   └┘
825  
826  lemma integral_add (f g : α →₁ₛ β) : integral (f + g) = integral f + integral g :=
id                                  
typ                                 
827  begin
828    simp only [integral],
829    rw ← simple_func.bintegral_add f.integrable g.integrable,
830    apply simple_func.bintegral_congr (f + g).integrable,
831      { exact f.integrable.add f.measurable g.measurable g.integrable },
st                                                                       └┘
832      { apply add_to_simple_func },
st                                  └┘
833  end
st   └─┘
834  
835  lemma integral_smul (r : ℝ) (f : α →₁ₛ β) : integral (r • f) = r • integral f :=
id                                                              
src                           
typ                                                             
836  begin
837    simp only [integral],
838    rw ← simple_func.bintegral_smul _ f.integrable,
839    apply simple_func.bintegral_congr (r • f).integrable,
id                                        
typ                                       
840      { exact integrable.smul _ f.integrable },
st                                              └┘
841      { apply smul_to_simple_func }
st                                   └─
842  end
st   ──┘
843  
844  lemma norm_integral_le_norm (f : α →₁ₛ β) : ∥ integral f ∥ ≤ ∥f∥ :=
id                                         
typ                                        
845  begin
846    rw [integral, norm_eq_bintegral],
847    exact f.to_simple_func.norm_bintegral_le_bintegral_norm f.integrable
848  end
st   └─┘
849  
850  /-- The Bochner integral over simple functions in l1 space as a continuous linear map. -/
851  def integral_clm : (α →₁ₛ β) →L[ℝ] β :=
id                                   
src                                  
typ                                  
852  linear_map.mk_continuous ⟨integral, integral_add, integral_smul⟩
853    1 (λf, le_trans (norm_integral_le_norm _) $ by rw one_mul)
854  
855  local notation `Integral` := @integral_clm α _ β _ _ _
856  
857  open continuous_linear_map
858  
859  lemma norm_Integral_le_one : ∥Integral∥ ≤ 1 :=
860  linear_map.mk_continuous_norm_le _ (zero_le_one) _
861  
862  section pos_part
863  
864  lemma pos_part_to_simple_func (f : α →₁ₛ ℝ) :
id                                           
src                                           
typ                                          
865    ∀ₘ a, f.pos_part.to_simple_func a = f.to_simple_func.pos_part a :=
id                                                                 
typ                                                                
866  begin
867    have eq : ∀ a, f.to_simple_func.pos_part a = max (f.to_simple_func a) 0 := λa, rfl,
id                                                                                
typ                                                                               
868    have ae_eq : ∀ₘ a, f.pos_part.to_simple_func a = max (f.to_simple_func a) 0,
id                     
typ                    
869    { filter_upwards [to_simple_func_eq_to_fun f.pos_part, pos_part_to_fun (f : α →₁ ℝ),
id                                                                                 
typ                                                                                
870        to_simple_func_eq_to_fun f],
871      simp only [mem_set_of_eq],
872      assume a h₁ h₂ h₃,
873      rw [h₁, coe_pos_part, h₂, ← h₃] },
st                                      └┘
874    filter_upwards [ae_eq],
875    simp only [mem_set_of_eq],
876    assume a h,
877    rw [h, eq]
st              
878  end
st   └─┘
879  
880  lemma neg_part_to_simple_func (f : α →₁ₛ ℝ) :
id                                           
src                                           
typ                                          
881    ∀ₘ a, f.neg_part.to_simple_func a = f.to_simple_func.neg_part a :=
id                                                                 
typ                                                                
882  begin
883    rw [simple_func.neg_part, measure_theory.simple_func.neg_part],
884    filter_upwards [pos_part_to_simple_func (-f), neg_to_simple_func f],
885    simp only [mem_set_of_eq],
886    assume a h₁ h₂,
887    rw h₁,
888    show max _ _ = max _ _,
889    rw h₂,
890    refl
891  end
st   └─┘
892  
893  lemma integral_eq_norm_pos_part_sub (f : α →₁ₛ ℝ) : f.integral = ∥f.pos_part∥ - ∥f.neg_part∥ :=
id                                                 
src                                                 
typ                                                
894  begin
895    -- Convert things in `L¹` to their `simple_func` counterpart
896    have ae_eq₁ : ∀ₘ a, f.to_simple_func.pos_part a = (f.pos_part).to_simple_func.map norm a,
id                      
typ                     
897    { filter_upwards [pos_part_to_simple_func f],
898      simp only [mem_set_of_eq],
899      assume a h,
900      rw [simple_func.map_apply, h],
901      conv_lhs { rw [← simple_func.pos_part_map_norm, simple_func.map_apply] } },
st                                                                                └┘
902    -- Convert things in `L¹` to their `simple_func` counterpart
903    have ae_eq₂ : ∀ₘ a, f.to_simple_func.neg_part a = (f.neg_part).to_simple_func.map norm a,
id                      
typ                     
904    { filter_upwards [neg_part_to_simple_func f],
905      simp only [mem_set_of_eq],
906      assume a h,
907      rw [simple_func.map_apply, h],
908      conv_lhs { rw [← simple_func.neg_part_map_norm, simple_func.map_apply] } },
st                                                                                └┘
909    -- Convert things in `L¹` to their `simple_func` counterpart
910    have ae_eq : ∀ₘ a, f.to_simple_func.pos_part a - f.to_simple_func.neg_part a =
id                     
typ                    
911      (f.pos_part).to_simple_func.map norm a - (f.neg_part).to_simple_func.map norm a,
912    { filter_upwards [ae_eq₁, ae_eq₂],
913      simp only [mem_set_of_eq],
914      assume a h₁ h₂,
915      rw [h₁, h₂] },
st                  └┘
916    rw [integral, norm_eq_bintegral, norm_eq_bintegral, ← simple_func.bintegral_sub],
917    { show f.to_simple_func.bintegral =
918        ((f.pos_part.to_simple_func).map norm - f.neg_part.to_simple_func.map norm).bintegral,
919      apply simple_func.bintegral_congr f.integrable,
920      { show integrable (f.pos_part.to_simple_func.map norm - f.neg_part.to_simple_func.map norm),
921        refine integrable_of_ae_eq _ _,
922        { exact (f.to_simple_func.pos_part - f.to_simple_func.neg_part) },
st                                                                         └┘
923        { exact (integrable.max_zero f.integrable).sub f.to_simple_func.pos_part.measurable
924          f.to_simple_func.neg_part.measurable (integrable.max_zero f.integrable.neg) },
st                                                                                       └┘
925        exact ae_eq },
st                     └┘
926      filter_upwards [ae_eq₁, ae_eq₂],
927      simp only [mem_set_of_eq],
928      assume a h₁ h₂, show _ = _ - _,
929      rw [← h₁, ← h₂],
930      have := f.to_simple_func.pos_part_sub_neg_part,
931      conv_lhs {rw ← this},
932      refl },
st            └┘
933    { refine integrable_of_ae_eq (integrable.max_zero f.integrable) ae_eq₁ },
st                                                                            └┘
934    { refine integrable_of_ae_eq (integrable.max_zero f.integrable.neg) ae_eq₂ }
st                                                                                └─
935  end
st   ──┘
936  
937  end pos_part
938  
939  end simple_func_integral
940  
941  end simple_func
942  
943  open simple_func
944  
945  variables [normed_space ℝ β] [normed_space ℝ γ] [complete_space β]
id                                             
src                                            
typ                                            
946  
947  section integration_in_l1
948  
949  local notation `to_l1` := coe_to_l1 α β ℝ
950  local attribute [instance] simple_func.normed_group simple_func.normed_space
951  
952  open continuous_linear_map
953  
954  /-- The Bochner integral in l1 space as a continuous linear map. -/
955  def integral_clm : (α →₁ β) →L[ℝ] β :=
id                                  
src                                 
typ                                 
956    integral_clm.extend to_l1 simple_func.dense_range simple_func.uniform_inducing
957  
958  /-- The Bochner integral in l1 space -/
959  def integral (f : α →₁ β) : β := (integral_clm).to_fun f
id                             
typ                            
960  
961  lemma integral_eq (f : α →₁ β) : integral f = (integral_clm).to_fun f := rfl
id                               
typ                              
962  
963  @[elim_cast] lemma integral_coe_eq_integral (f : α →₁ₛ β) :
id                                                         
typ                                                        
doc    └───────┘
964    integral (f : α →₁ β) = f.integral :=
id                       
typ                      
965  by { refine uniformly_extend_of_ind _ _ _ _, exact simple_func.integral_clm.uniform_continuous }
st                                                                                                  └┘
966  
967  variables (α β)
968  @[simp] lemma integral_zero : integral (0 : α →₁ β) = 0 :=
id                                                   
typ                                                  
doc    └──┘
969  map_zero integral_clm
970  variables {α β}
971  
972  lemma integral_add (f g : α →₁ β) : integral (f + g) = integral f + integral g :=
id                                 
typ                                
973  map_add integral_clm f g
974  
975  lemma integral_neg (f : α →₁ β) : integral (-f) = - integral f :=
id                               
typ                              
976  map_neg integral_clm f
977  
978  lemma integral_sub (f g : α →₁ β) : integral (f - g) = integral f - integral g :=
id                                 
typ                                
979  map_sub integral_clm f g
980  
981  lemma integral_smul (r : ℝ) (f : α →₁ β) : integral (r • f) = r • integral f :=
id                                                             
src                           
typ                                                            
982  map_smul r integral_clm f
id            
typ           
983  
984  local notation `Integral` := @integral_clm α _ β _ _ _ _
985  local notation `sIntegral` := @simple_func.integral_clm α _ β _ _ _
986  
987  lemma norm_Integral_le_one : ∥Integral∥ ≤ 1 :=
988  calc ∥Integral∥ ≤ 1 * ∥sIntegral∥ :
989    op_norm_extend_le _ _ _ $ λs, by {rw one_mul, refl}
st                                                       └┘
990    ... = ∥sIntegral∥ : one_mul _
991    ... ≤ 1 : norm_Integral_le_one
992  
993  lemma norm_integral_le (f : α →₁ β) : ∥integral f∥ ≤ ∥f∥ :=
id                                   
typ                                  
994  calc ∥integral f∥ = ∥Integral f∥ : rfl
995    ... ≤ ∥Integral∥ * ∥f∥ : le_op_norm _ _
996    ... ≤ 1 * ∥f∥ : mul_le_mul_of_nonneg_right norm_Integral_le_one $ norm_nonneg _
997    ... = ∥f∥ : one_mul _
998  
999  section pos_part
1000  
1001  lemma integral_eq_norm_pos_part_sub (f : α →₁ ℝ) : integral f = ∥pos_part f∥ - ∥neg_part f∥ :=
id                                                
src                                                
typ                                               
1002  begin
1003    -- Use `is_closed_property` and `is_closed_eq`
1004    refine @is_closed_property _ _ _ (coe : (α →₁ₛ ℝ) → (α →₁ ℝ))
1005      (λ f : α →₁ ℝ, integral f = ∥pos_part f∥ - ∥neg_part f∥)
1006      l1.simple_func.dense_range (is_closed_eq _ _) _ f,
1007    { exact cont _ },
st                    └┘
1008    { refine continuous.sub (continuous_norm.comp l1.continuous_pos_part)
1009        (continuous_norm.comp l1.continuous_neg_part) },
st                                                       └┘
1010    -- Show that the property holds for all simple functions in the `L¹` space.
1011    { assume s,
1012      norm_cast,
1013      rw [← simple_func.norm_eq, ← simple_func.norm_eq],
1014      exact simple_func.integral_eq_norm_pos_part_sub _}
st                                                        └─
1015  end
st   ──┘
1016  
1017  end pos_part
1018  
1019  end integration_in_l1
1020  
1021  end l1
1022  
1023  variables [normed_group β] [second_countable_topology β] [normed_space ℝ β] [complete_space β]
id              └┘  └──┘  └┘                                                
src             └┘  └──┘  └┘                                                
typ             └┘  └──┘  └┘                                                
doc             └┘  └──┘  └┘
1024            [normed_group γ] [second_countable_topology γ] [normed_space ℝ γ] [complete_space γ]
id              └──────────┘                                                
src             └──────────┘                                                
typ             └──────────┘                                                
doc             └──────────┘
1025  
1026  /-- The Bochner integral -/
1027  def integral (f : α → β) : β :=
id                            
typ                           
1028  if hf : measurable f ∧ integrable f
id                                    
typ                                   
1029  then (l1.of_fun f hf.1 hf.2).integral
id                   
typ                  
1030  else 0
1031  
1032  notation `∫` binders `, ` r:(scoped f, integral f) := r
1033  
1034  section properties
1035  
1036  open continuous_linear_map measure_theory.simple_func
1037  
1038  variables {f g : α → β}
1039  
1040  lemma integral_eq (f : α → β) (h₁ : measurable f) (h₂ : integrable f) :
id                                                                   
typ                                                                  
1041    (∫ a, f a) = (l1.of_fun f h₁ h₂).integral :=
id                          
typ                         
1042  dif_pos ⟨h₁, h₂⟩
1043  
1044  lemma integral_undef (h : ¬ (measurable f ∧ integrable f)) : (∫ a, f a) = 0 :=
id                                                                  
src                                           
typ                                                                 
1045  dif_neg h
1046  
1047  lemma integral_non_integrable (h : ¬ integrable f) : (∫ a, f a) = 0 :=
id                                                            
src                                     
typ                                                           
1048  integral_undef $ not_and_of_not_right _ h
1049  
1050  lemma integral_non_measurable (h : ¬ measurable f) : (∫ a, f a) = 0 :=
id                                                            
src                                     
typ                                                           
1051  integral_undef $ not_and_of_not_left _ h
1052  
1053  variables (α β)
1054  @[simp] lemma integral_zero : (∫ a:α, (0:β)) = 0 :=
id                                           
typ                                          
doc    └──┘
1055  by rw [integral_eq, l1.of_fun_zero, l1.integral_zero]
st                                                       
1056  
1057  variables {α β}
1058  
1059  lemma integral_add
1060    (hfm : measurable f) (hfi : integrable f) (hgm : measurable g) (hgi : integrable g) :
id                                                                                   
typ                                                                                  
1061    (∫ a, f a + g a) = (∫ a, f a) + (∫ a, g a) :=
id                                   
typ                                  
1062  by rw [integral_eq, integral_eq f hfm hfi, integral_eq g hgm hgi, l1.of_fun_add, l1.integral_add]
id                                                         
typ                                                        
st                                                                                                   
1063  
1064  lemma integral_neg (f : α → β) : (∫ a, -f a) = - (∫ a, f a) :=
id                                                     
typ                                                    
1065  begin
1066    by_cases hf : measurable f ∧ integrable f,
1067    { rw [integral_eq f hf.1 hf.2, integral_eq (λa, - f a) hf.1.neg hf.2.neg, l1.of_fun_neg,
id                                                     
typ                                                    
1068      l1.integral_neg] },
st                       └┘
1069    { have hf' : ¬(measurable (λa, -f a) ∧ integrable (λa, -f a)),
id                                                           
typ                                                          
1070      { rwa [measurable_neg_iff, integrable_neg_iff] },
st                                                      └┘
1071      rw [integral_undef hf, integral_undef hf', neg_zero] }
st                                                           └─
1072  end
st   ──┘
1073  
1074  lemma integral_sub
1075    (hfm : measurable f) (hfi : integrable f) (hgm : measurable g) (hgi : integrable g) :
id                                                                                   
typ                                                                                  
1076    (∫ a, f a - g a) = (∫ a, f a) - (∫ a, g a) :=
id                                   
typ                                  
1077  by simp only [sub_eq_add_neg, integral_neg, integral_add, measurable_neg_iff, integrable_neg_iff, *]
1078  
1079  lemma integral_smul (r : ℝ) (f : α → β) : (∫ a, r • (f a)) = r • (∫ a, f a) :=
id                                                                  
src                           
typ                                                                 
1080  begin
1081    by_cases hf : measurable f ∧ integrable f,
1082    { rw [integral_eq f hf.1 hf.2, integral_eq (λa, r • (f a)), l1.of_fun_smul, l1.integral_smul] },
id                                                       
typ                                                      
st                                                                                                  └┘
1083    { by_cases hr : r = 0,
id                     
typ                    
1084      { simp only [hr, measure_theory.integral_zero, zero_smul] },
st                                                                 └┘
1085      have hf' : ¬(measurable (λa, r • f a) ∧ integrable (λa, r • f a)),
id                                                                
typ                                                               
1086      { rwa [← measurable_smul_iff hr f, ← integrable_smul_iff hr f] at hf },
id                                                                  
typ                                                                 
st                                                                            └┘
1087      rw [integral_undef hf, integral_undef hf', smul_zero] }
st                                                            └─
1088  end
st   ──┘
1089  
1090  lemma integral_mul_left (r : ℝ) (f : α → ℝ) : (∫ a, r * (f a)) = r * (∫ a, f a) :=
id                                                                      
src                                          
typ                                                                     
1091  integral_smul r f
id                  
typ                 
1092  
1093  lemma integral_mul_right (r : ℝ) (f : α → ℝ) : (∫ a, (f a) * r) = (∫ a, f a) * r :=
id                                                                         
src                                            
typ                                                                        
1094  by { simp only [mul_comm], exact integral_mul_left r f }
id                                                       
typ                                                      
st                                                          └┘
1095  
1096  lemma integral_div (r : ℝ) (f : α → ℝ) : (∫ a, (f a) / r) = (∫ a, f a) / r :=
id                                                                  
src                                     
typ                                                                 
1097  integral_mul_right r⁻¹ f
id                         
typ                        
1098  
1099  lemma integral_congr_ae (hfm : measurable f) (hgm : measurable g) (h : ∀ₘ a, f a = g a) :
id                                                                                  
typ                                                                                 
1100     (∫ a, f a) = (∫ a, g a) :=
id                      
typ                     
1101  begin
1102    by_cases hfi : integrable f,
1103    { have hgi : integrable g := integrable_of_ae_eq hfi h,
id                             
typ                            
1104      rw [integral_eq f hfm hfi, integral_eq g hgm hgi, (l1.of_fun_eq_of_fun f g hfm hfi hgm hgi).2 h] },
id                                                                             
typ                                                                            
st                                                                                                       └┘
1105    { have hgi : ¬ integrable g, { rw integrable_congr_ae h at hfi, exact hfi },
id                               
typ                              
st                                                                               └┘
1106      rw [integral_non_integrable hfi, integral_non_integrable hgi] },
st                                                                    └┘
1107  end
st   └─┘
1108  
1109  lemma norm_integral_le_lintegral_norm (f : α → β) :
id                                                 
typ                                                
1110    ∥(∫ a, f a)∥ ≤ ennreal.to_real (∫⁻ a, ennreal.of_real ∥f a∥) :=
id                   └┘  └┘  └┘         └┘  └┘  └┘  └┘     
src                     └┘  └┘  └┘          └┘  └┘  └┘  └┘
typ                  └┘  └┘  └┘         └┘  └┘  └┘  └┘     
doc                     └┘  └┘  └┘          └┘  └┘  └┘  └┘
1111  begin
1112    by_cases hf : measurable f ∧ integrable f,
1113    { rw [integral_eq f hf.1 hf.2, ← l1.norm_of_fun_eq_lintegral_norm f hf.1 hf.2],
id                                                                      
typ                                                                     
1114      exact l1.norm_integral_le _ },
st                                   └┘
1115    { rw [integral_undef hf, _root_.norm_zero],
1116      exact to_real_nonneg }
st                            └─
1117  end
st   ──┘
1118  
1119  /-- Lebesgue dominated convergence theorem provides sufficient conditions under which almost
1120    everywhere convergence of a sequence of functions implies the convergence of their integrals. -/
1121  theorem tendsto_integral_of_dominated_convergence {F : ℕ → α → β} {f : α → β} (bound : α → ℝ)
id                                                                                         
src                                                                                            
typ                                                                                        
1122    (F_measurable : ∀ n, measurable (F n))
id                                      
typ                                     
1123    (f_measurable : measurable f)
id                                
typ                               
1124    (bound_integrable : integrable bound)
id                                    └─┘ 
typ                                   └─┘ 
1125    (h_bound : ∀ n, ∀ₘ a, ∥F n a∥ ≤ bound a)
id                                 └───┘ 
typ                                └───┘ 
1126    (h_lim : ∀ₘ a, tendsto (λ n, F n a) at_top (𝓝 (f a))) :
id                                                 
typ                                                
1127    tendsto (λn, ∫ a, F n a) at_top (𝓝 $ (∫ a, f a)) :=
id                                             
typ                                            
1128  begin
1129    /- To show `(∫ a, F n a) --> (∫ f)`, suffices to show `∥∫ a, F n a - ∫ f∥ --> 0` -/
1130    rw tendsto_iff_norm_tendsto_zero,
1131    /- But `0 ≤ ∥∫ a, F n a - ∫ f∥ = ∥∫ a, (F n a - f a) ∥ ≤ ∫ a, ∥F n a - f a∥, and thus we apply the
1132      sandwich theorem and prove that `∫ a, ∥F n a - f a∥ --> 0` -/
1133    have zero_tendsto_zero : tendsto (λn:ℕ, (0 : ℝ)) at_top (𝓝 0) := tendsto_const_nhds,
1134    have lintegral_norm_tendsto_zero :
1135      tendsto (λn, ennreal.to_real $ ∫⁻ a, ennreal.of_real ∥F n a - f a∥) at_top (𝓝 0) :=
id                   └─────────────┘        └─────────────┘         
src                   └─────────────┘         └─────────────┘
typ                  └─────────────┘        └─────────────┘         
doc                   └─────────────┘         └─────────────┘
1136    tendsto.comp (tendsto_to_real (zero_ne_top))
1137      (tendsto_lintegral_norm_of_dominated_convergence
1138        F_measurable f_measurable bound_integrable h_bound h_lim),
1139    -- Use the sandwich theorem
1140    refine tendsto_of_tendsto_of_tendsto_of_le_of_le zero_tendsto_zero lintegral_norm_tendsto_zero _ _,
1141    -- Show `0 ≤ ∥∫ a, F n a - ∫ f∥` for all `n`
1142    { simp only [filter.eventually_at_top, norm_nonneg, forall_true_iff, exists_const] },
st                                                                                        └┘
1143    -- Show `∥∫ a, F n a - ∫ f∥ ≤ ∫ a, ∥F n a - f a∥` for all `n`
1144    { simp only [filter.eventually_at_top],
1145      use 0,
1146      assume n hn,
1147      have h₁ : integrable (F n) := integrable_of_integrable_bound bound_integrable (h_bound _),
id                              
typ                             
1148      have h₂ : integrable f := integrable_of_dominated_convergence bound_integrable h_bound h_lim,
id                            
typ                           
1149      rw ← integral_sub (F_measurable _) h₁ f_measurable h₂,
1150      exact norm_integral_le_lintegral_norm _ }
st                                               └─
1151  end
st   ──┘
1152  
1153  /-- Lebesgue dominated convergence theorem for filters with a countable basis -/
1154  lemma tendsto_integral_filter_of_dominated_convergence {ι} {l : filter ι}
id                                                                     └┘   
src                                                                    └┘
typ                                                                    └┘   
1155    {F : ι → α → β} {f : α → β} (bound : α → ℝ)
id                                        
src                                             
typ                                       
1156    (hl_cb : l.has_countable_basis)
id              
typ             
1157    (hF_meas : ∀ᶠ n in l, measurable (F n))
id                                      
typ                                     
1158    (f_measurable : measurable f)
id                                
typ                               
1159    (h_bound : ∀ᶠ n in l, ∀ₘ a, ∥F n a∥ ≤ bound a)
id                                       └─┘ 
typ                                      └─┘ 
1160    (bound_integrable : integrable bound)
id                                     └┘
typ                                    └┘
1161    (h_lim : ∀ₘ a, tendsto (λ n, F n a) l (𝓝 (f a))) :
id                                            
typ                                           
1162    tendsto (λn, ∫ a, F n a) l (𝓝 $ (∫ a, f a)) :=
id                                       
typ                                      
1163  begin
1164    rw hl_cb.tendsto_iff_seq_tendsto,
1165    { intros x xl,
1166      have hxl, { rw tendsto_at_top' at xl, exact xl },
st                                                      └┘
1167      have h := inter_mem_sets hF_meas h_bound,
1168      replace h := hxl _ h,
1169      rcases h with ⟨k, h⟩,
1170      rw ← tendsto_add_at_top_iff_nat k,
id                                       
typ                                      
1171      refine tendsto_integral_of_dominated_convergence _ _ _ _ _ _,
1172      { exact bound },
id               └───┘
typ              └───┘
st                     └┘
1173      { intro, refine (h _ _).1, exact nat.le_add_left _ _ },
st                                                            └┘
1174      { assumption },
st                    └┘
1175      { assumption },
st                    └┘
1176      { intro, refine (h _ _).2, exact nat.le_add_left _ _ },
st                                                            └┘
1177      { filter_upwards [h_lim],
1178        simp only [mem_set_of_eq],
1179        assume a h_lim,
1180        apply @tendsto.comp _ _ _ (λn, x (n + k)) (λn, F n a),
id                                                       
typ                                                      
1181        { assumption },
st                      └┘
1182        rw tendsto_add_at_top_iff_nat,
1183        assumption } },
st                    └──┘
1184  end
st   └─┘
1185  
1186  /-- The Bochner integral of a real-valued function `f : α → ℝ` is the difference between the
1187    integral of the positive part of `f` and the integral of the negative part of `f`.  -/
1188  lemma integral_eq_lintegral_max_sub_lintegral_min {f : α → ℝ}
id                                                             
src                                                             
typ                                                            
1189    (hfm : measurable f) (hfi : integrable f) : (∫ a, f a) =
id                                                     
typ                                                    
1190    ennreal.to_real (∫⁻ a, ennreal.of_real $ max (f a) 0) -
id       └┘  └┘  └┘         └┘  └┘  └┘  └┘          
src      └┘  └┘  └┘          └┘  └┘  └┘  └┘
typ      └┘  └┘  └┘         └┘  └┘  └┘  └┘          
doc      └┘  └┘  └┘          └┘  └┘  └┘  └┘
1191    ennreal.to_real (∫⁻ a, ennreal.of_real $ - min (f a) 0) :=
id     └─┘  └┘  └┘  └┘         └┘  └┘  └┘             
src    └─┘  └┘  └┘  └┘          └┘  └┘  └┘
typ    └─┘  └┘  └┘  └┘         └┘  └┘  └┘             
doc    └─┘  └┘  └┘  └┘          └┘  └┘  └┘
1192  let f₁ : α →₁ ℝ := l1.of_fun f hfm hfi in
id                              
src                
typ                             
1193  -- Go to the `L¹` space
1194  have eq₁ : ennreal.to_real (∫⁻ a, ennreal.of_real $ max (f a) 0) = ∥l1.pos_part f₁∥ :=
id              └┘ └┘ └┘ └┘ └┘         └┘ └┘ └┘ └┘          
src             └┘ └┘ └┘ └┘ └┘          └┘ └┘ └┘ └┘ 
typ             └┘ └┘ └┘ └┘ └┘         └┘ └┘ └┘ └┘          
doc             └┘ └┘ └┘ └┘ └┘          └┘ └┘ └┘ └┘ 
1195  begin
1196    rw l1.norm_eq_norm_to_fun,
1197    congr' 1,
1198    apply lintegral_congr_ae,
1199    filter_upwards [l1.pos_part_to_fun f₁, l1.to_fun_of_fun f hfm hfi],
id                                                             
typ                                                            
1200    simp only [mem_set_of_eq],
1201    assume a h₁ h₂,
1202    rw [h₁, h₂, real.norm_eq_abs, abs_of_nonneg],
1203    exact le_max_right _ _
1204  end,
st   └─┘
1205  -- Go to the `L¹` space
1206  have eq₂ : ennreal.to_real (∫⁻ a, ennreal.of_real $ -min (f a) 0) = ∥l1.neg_part f₁∥ :=
id              └─────────────┘       └─────────────┘          
src             └─────────────┘        └─────────────┘
typ             └─────────────┘       └─────────────┘          
doc             └─────────────┘        └─────────────┘
1207  begin
1208    rw l1.norm_eq_norm_to_fun,
1209    congr' 1,
1210    apply lintegral_congr_ae,
1211    filter_upwards [l1.neg_part_to_fun_eq_min f₁, l1.to_fun_of_fun f hfm hfi],
id                                                                    
typ                                                                   
1212    simp only [mem_set_of_eq],
1213    assume a h₁ h₂,
1214    rw [h₁, h₂, real.norm_eq_abs, abs_of_nonneg],
1215    rw [min_eq_neg_max_neg_neg, _root_.neg_neg, neg_zero],
1216    exact le_max_right _ _
1217  end,
st   └─┘
1218  begin
1219    rw [eq₁, eq₂, integral, dif_pos],
1220    exact l1.integral_eq_norm_pos_part_sub _,
1221    { exact ⟨hfm, hfi⟩ }
st                        └─
1222  end
st   ──┘
1223  
1224  lemma integral_eq_lintegral_of_nonneg_ae {f : α → ℝ} (hf : ∀ₘ a, 0 ≤ f a) (hfm : measurable f) :
id                                                                                          
src                                                    
typ                                                                                         
1225    (∫ a, f a) = ennreal.to_real (∫⁻ a, ennreal.of_real $ f a) :=
id                 └┘  └┘  └┘           └┘  └┘  └┘      
src                   └┘  └┘  └┘            └┘  └┘  └┘
typ                └┘  └┘  └┘           └┘  └┘  └┘      
doc                   └┘  └┘  └┘            └┘  └┘  └┘
1226  begin
1227    by_cases hfi : integrable f,
1228    { rw integral_eq_lintegral_max_sub_lintegral_min hfm hfi,
1229      have h_min : (∫⁻ a, ennreal.of_real (-min (f a) 0)) = 0,
id                          └─────────────┘        
src                          └─────────────┘
typ                         └─────────────┘        
doc                          └─────────────┘
1230      { rw lintegral_eq_zero_iff,
1231        { filter_upwards [hf],
1232          simp only [mem_set_of_eq],
1233          assume a h,
1234          simp only [min_eq_right h, neg_zero, ennreal.of_real_zero] },
st                                                                      └┘
1235        { refine measurable_of_real.comp
1236            ((measurable.neg measurable_id).comp $ measurable.min hfm measurable_const) } },
st                                                                                         └──┘
1237      have h_max : (∫⁻ a, ennreal.of_real (max (f a) 0)) = (∫⁻ a, ennreal.of_real $ f a),
id                                                                 └─────────────┘   
src                                                                  └─────────────┘
typ                                                                └─────────────┘   
doc                                                                  └─────────────┘
1238      { apply lintegral_congr_ae,
1239        filter_upwards [hf],
1240        simp only [mem_set_of_eq],
1241        assume a h,
1242        rw max_eq_left h },
st                          └┘
1243      rw [h_min, h_max, zero_to_real, _root_.sub_zero] },
st                                                       └┘
1244    { rw integral_non_integrable hfi,
1245      rw [integrable_iff_norm, lt_top_iff_ne_top, ne.def, not_not] at hfi,
1246      have : (∫⁻ (a : α), ennreal.of_real (f a)) = (∫⁻ a, ennreal.of_real ∥f a∥),
id                                                         └─────────────┘  
src                                                          └─────────────┘
typ                                                        └─────────────┘  
doc                                                          └─────────────┘
1247      { apply lintegral_congr_ae,
1248        filter_upwards [hf],
1249        simp only [mem_set_of_eq],
1250        assume a h,
1251        rw [real.norm_eq_abs, abs_of_nonneg h] },
st                                               └┘
1252      rw [this, hfi], refl }
st                            └─
1253  end
st   ──┘
1254  
1255  lemma integral_nonneg_of_nonneg_ae {f : α → ℝ} (hf : ∀ₘ a, 0 ≤ f a) : 0 ≤ (∫ a, f a) :=
id                                                                              
src                                              
typ                                                                             
1256  begin
1257    by_cases hfm : measurable f,
1258    { rw integral_eq_lintegral_of_nonneg_ae hf hfm, exact to_real_nonneg },
st                                                                          └┘
1259    { rw integral_non_measurable hfm }
st                                      └─
1260  end
st   ──┘
1261  
1262  lemma integral_nonpos_of_nonpos_ae {f : α → ℝ} (hf : ∀ₘ a, f a ≤ 0) : (∫ a, f a) ≤ 0 :=
id                                                                          
src                                              
typ                                                                         
1263  begin
1264    have hf : ∀ₘ a, 0 ≤ (-f) a,
id                          
typ                         
1265    { filter_upwards [hf], simp only [mem_set_of_eq], assume a h, rwa [pi.neg_apply, neg_nonneg] },
st                                                                                                  └┘
1266    have : 0 ≤ (∫ a, -f a) := integral_nonneg_of_nonneg_ae hf,
id                      
typ                     
1267    rwa [integral_neg, neg_nonneg] at this,
1268  end
st   └─┘
1269  
1270  lemma integral_le_integral_ae {f g : α → ℝ} (hfm : measurable f) (hfi : integrable f)
id                                                                                   
src                                           
typ                                                                                  
1271    (hgm : measurable g) (hgi : integrable g) (h : ∀ₘ a, f a ≤ g a) : (∫ a, f a) ≤ (∫ a, g a) :=
id                                                                                
typ                                                                               
1272  le_of_sub_nonneg
1273  begin
1274    rw ← integral_sub hgm hgi hfm hfi,
1275    apply integral_nonneg_of_nonneg_ae,
1276    filter_upwards [h],
1277    simp only [mem_set_of_eq],
1278    assume a,
1279    exact sub_nonneg_of_le
1280  end
st   └─┘
1281  
1282  lemma integral_le_integral {f g : α → ℝ} (hfm : measurable f) (hfi : integrable f)
id                                                                                
src                                        
typ                                                                               
1283    (hgm : measurable g) (hgi : integrable g) (h : ∀ a, f a ≤ g a) : (∫ a, f a) ≤ (∫ a, g a) :=
id                                                                               
typ                                                                              
1284  integral_le_integral_ae hfm hfi hgm hgi $ univ_mem_sets' h
1285  
1286  lemma norm_integral_le_integral_norm (f : α → β) : ∥(∫ a, f a)∥ ≤ ∫ a, ∥f a∥ :=
id                                                                      
typ                                                                     
1287  have le_ae : ∀ₘ (a : α), 0 ≤ ∥f a∥ := by filter_upwards [] λa, norm_nonneg _,
id                                                            
typ                                                           
1288  classical.by_cases
1289  ( λh : measurable f,
id                     
typ                    
1290    calc ∥(∫ a, f a)∥ ≤ ennreal.to_real (∫⁻ a, ennreal.of_real ∥f a∥) : norm_integral_le_lintegral_norm _
id                      └─────────────┘       └─────────────┘   
src                        └─────────────┘        └─────────────┘
typ                     └─────────────┘       └─────────────┘   
doc                        └─────────────┘        └─────────────┘
1291      ... = ∫ a, ∥f a∥ : (integral_eq_lintegral_of_nonneg_ae le_ae $ measurable.norm h).symm )
id                   
typ                  
1292  ( λh : ¬measurable f,
id                      
typ                     
1293    begin
1294      rw [integral_non_measurable h, _root_.norm_zero],
1295      exact integral_nonneg_of_nonneg_ae le_ae
1296    end )
st     └─┘
1297  
1298  lemma integral_finset_sum {ι} (s : finset ι) {f : ι → α → β}
id                                      └┘  └┘               
src                                     └┘  └┘
typ                                     └┘  └┘               
doc                                     └┘  └┘
1299    (hfm : ∀ i, measurable (f i)) (hfi : ∀ i, integrable (f i)) :
id                                                         
typ                                                        
1300    (∫ a, s.sum (λ i, f i a)) = s.sum (λ i, ∫ a, f i a) :=
id                                             
typ                                            
1301  begin
1302    refine finset.induction_on s _ _,
1303    { simp only [integral_zero, finset.sum_empty] },
st                                                   └┘
1304    { assume i s his ih,
1305      simp only [his, finset.sum_insert, not_false_iff],
id                                          └───────────┘
src                                         └───────────┘
typ                                         └───────────┘
1306      rw [integral_add (hfm _) (hfi _) (measurable_finset_sum s hfm)
1307          (integrable_finset_sum s hfm hfi), ih] }
id                                  
typ                                 
st                                                 └─
1308  end
st   ──┘
1309  
1310  end properties
1311  
1312  mk_simp_attribute integral_simps "Simp set for integral rules."
1313  
1314  attribute [integral_simps] integral_neg integral_smul l1.integral_add l1.integral_sub
doc             └────────────┘
1315    l1.integral_smul l1.integral_neg
1316  
1317  attribute [irreducible] integral l1.integral
src             └─────────┘
doc             └─────────┘
1318  
1319  end measure_theory